equality (definitional?, propositional, computational, judgemental, extensional, intensional, decidable)
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 $X \subseteq A \times B$ consisting of pairs $(a,b)$ such that the equation $f(a) = g(b)$ hold.
A pullback is therefore the categorical semantics of an equation.
This construction comes up, for example, when $A$ and $B$ are fiber bundles over $C$: then $X$ as defined above is the product of $A$ and $B$ in the category of fiber bundles over $C$. For this reason, a pullback is sometimes called a fibered product (or fiber product or fibre product).
In this case, the fiber of $A \times_C B$ over a (generalized) element $x$ of $C$ is the ordinary product of the fibers of $A$ and $B$ over $x$. In other words, the fiber product is the product taken fiber-wise. Of course, the fiber of $A$ at the generalized element $x\colon I \to C$ is itself a fibre product $I \times_C A$; the terminology depends on your point of view.
Note that there are maps $p_A : X \to A$, $p_B : X \to B$ sending any $(a,b) \in X$ to $a$ and $b$, 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 $h: Y \to X$ 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 $x$ 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 $Set$.
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 $C$ is the same as a pushout in the opposite category $C^{op}$.
In type theory a pullback $P$ in
is given by the dependent sum over the dependent equality type
If products exist in $C$, then the pullback
is equivalently the equalizer
of the two morphisms induced by $f$ and $g$ out of the product of $a$ with $b$.
Consider a pasting 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 left-hand one is a pullback if and only if the outer square is.
Proof. Pasting a morphism $x \to a$ 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 $x \to a$ includes a morphism into $b$, which if $b$ is a pullback induces the same commuting square over $d \to e \to f$ and $c \to d$. 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 $i : a \to b$ be a split monomorphism with retract $p : b \to a$ and consider
Then the left square and the outer rectangle are pullbacks but the right square cannot be a pullback unless $i$ was already an isomorphism.
The saturation of the class of pullbacks is the class of limits over categories $C$ whose groupoid reflection $\Pi_1(C)$ is trivial and such that $C$ is L-finite.