equality (definitional, propositional, computational, judgemental, extensional?, intensional?, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
In the category Set a ‘pullback’ is a subset of the cartesian product of two sets. Given a diagram of sets and functions like this:
the ‘pullback’ of this diagram is the subset consisting of pairs such that the equation holds.
A pullback is therefore the categorical semantics of an equation.
This construction comes up, for example, when and are fiber bundles over : then as defined above is the product of and in the category of fiber bundles over . For this reason, a pullback is sometimes called a fibered product (or fiber product or fibre product).
In this case, the fiber of over a (generalized) element of is the ordinary product of the fibers of and over . In other words, the fiber product is the product taken fiber-wise. Of course, the fiber of at the generalized element is itself a fibre product ; the terminology depends on your point of view.
Note that there are maps , sending any to and , respectively. These maps make this square commute:
In fact, the pullback is the universal solution to finding a commutative square like this. In other words, given any commutative square
there is a unique function such that
and
Since this universal property expresses the concept of pullback purely arrow-theoretically, we can formulate it in any category. It is, in fact, a simple special case of a limit.
A pullback is a limit of a diagram like this:
Such a diagram is also called a pullback diagram or a cospan. If the limit exists, we obtain a commutative square
and the object is also called the pullback. It is well defined up to unique isomorphism. It has the universal property already described above in the special case of the category .
The last commutative square above is called a pullback square.
The concept of pullback is dual to the concept of pushout: that is, a pullback in is the same as a pushout in the opposite category .
Let be a category, with and coterminal arrows in as below
A pullback of and consists of an object together with arrows and such that the following diagram commutes universally
This means that for any other object with arrows and such that
commutes, there exists a unique arrow such that
commutes.
In type theory a pullback in
is given by the dependent sum over the dependent equality type
(pullbacks as equalizers)
If products exist in , then the pullback
is equivalently the equalizer
of the two morphisms induced by and out of the product of with .
As a consequence of the above, any category with binary products and equalizers has pullbacks. Conversely any category with binary products and pullbacks has equalizers: the equalizer of is the pullback of and .
(pullbacks preserve monomorphisms and isomorphisms)
Pullbacks preserve monomorphisms and isomorphisms:
If
is a pullback square in some category then:
if is a monomorphism then is a monomorphism;
if is an isomorphism then is an isomorphism.
On the other hand that is a monomorphism does not imply that is a monomorphism.
In any category consider a diagram of the form
There are three commuting squares: the two inner ones and the outer one.
Suppose the right-hand inner square is a pullback, then:
The square on the left is a pullback if and only if the outer square is.
Pasting a morphism with the outer square gives rise to a commuting square over the (composite) bottom and right edges of the diagram. The square over the cospan in the left-hand inner square arising from includes a morphism into , which if is a pullback induces the same commuting square over and . So one square is universal iff the other is.
The converse implication does not hold: it may happen that the outer and the left square are pullbacks, but not the right square.
For instance let be a split monomorphism with retract and consider
Then the left square and the outer rectangle are pullbacks but the right square cannot be a pullback unless was already an isomorphism.
On the other hand, in the (∞,1)-category of ∞-groupoids, there is a sort of “partial converse”; see at homotopy pullback – homotopy fiber characterizationullback#HomotopyFiberCharacterization).
The saturation of the class of pullbacks is the class of limits over categories whose groupoid reflection is trivial and such that is L-finite.
If is a morphism in a category with pullbacks, there is an induced pullback functor , sometimes also called base change.
Notions of pullback:
pullback, fiber product (limit over a cospan)
lax pullback, comma object (lax limit over a cospan)
(∞,1)-pullback, homotopy pullback, ((∞,1)-limit over a cospan)
Early use of the terminology “pullback”:
Textbook accounts:
Saunders MacLane, p. 71 in: Categories for the Working Mathematician, Springer (1971) [doi:10.1007/978-1-4757-4721-8]
Francis Borceux, Section 2.5 in Vol. 1: Basic Category Theory of: Handbook of Categorical Algebra, Encyclopedia of Mathematics and its Applications 50 Cambridge University Press (1994) (doi:10.1017/CBO9780511525858)
See also:
In view of more general finite limits and L-finite limits, including the completion of a category under pullbacks:
Morphisms admitting pullbacks along them are called carrable in some places, for instance, the following:
They are called quarrable in:
Last revised on September 19, 2025 at 13:18:18. See the history of this page for a list of all contributions to it.