**(a)**- Let
**f**,**g**:*X*\rightrightarrows*Y*be aof maps in a category*parallel pair**S*. Then an object*E*together with a morphism**m**:*E*®*X*is anof*equaliser***f**and**g**if**m**;**f**=**m**;**g**, and whenever**a**:G®*X*is another morphism such that**a**;**f**=**a**;**g**there is a unique map**h**:G®*E*with**a**=**h**;**m**. **(b)**- Let
**f**:*X*®*Z*and**g**:*Y*®*Z*be two maps in a category. Then an object*P*together with a pair of maps p_{0}:*P*®*X*and p_{1}:*P*®*Y*is aif p*pullback*_{0};**f**= p_{1};**g**and whenever**a**:G®*X*and**b**:G®*Y*also satisfy**a**;**f**=**b**;**g**there is a unique map**h**:G®*P*such that**h**;p_{0}=**a**and**h**;p_{1}=**b**.

displaymath omitted diagram environment omitted diagram environment

Pullbacks and equalisers are unique up to unique isomorphism where they
exist, *cf* Theorem 4.5.6.

The pullback and mediator are written *X*×_{Z}*Y* and **a**,**b**.
However, one should remember that this notation hides not only the projection
maps (which were already absent from the product and exponential notations
we have used) but also the maps **f** and **g** which are part of the
data. The object *X*×_{Z}*Y* or the map p_{1}:*X*×_{Z}*Y*® *Y* is also
called the pullback of **f** ** along** or

Pullbacks are often indicated with the right angle symbol, which was suggested
by William Butler in 1974 and popularised by Peter Freyd. In Section
9.4 we will no longer be able to afford the space for it,
and will instead adopt the convention that the ubiquitous pullbacks are
drawn as *parallelograms*. This emphasises how pullbacks do ``parallel
translation'' of structure, in particular by substitution in syntax.

There is no widely used notation for an equaliser, but Freyd and Scedrov [
FS90] write \rightarrowtail ^{\f}_{g}
or just \rightarrowtail ^{·}_{·} for the map **m**. The
hook notation will be discussed in the next section.

The following easy result will turn out to be *extremely* useful:

LEMMA 5.1.2 Suppose that the two squares commute below, and that the one on the right is a pullback.

omitted diagram environment

Then the rectangle is a pullback iff the left hand square is. []

**(a)**- Pullbacks in a poset are just meets, but of pairs with a common
upper bound (Exercises 3.5,
3.20, 3.34 and
4.51). Since all squares commute, what the
bound
*is*doesn't matter, only that it*exists*. Again, since any two parallel maps are equal, they trivially have an equaliser: the identity. **(b)**- A parallel pair
**f**,**g**:[[(*x*)\vec]:[(*X*)\vec]] \rightrightarrows [[(*y*)\vec]:[(*Y*)\vec]] in the category of contexts and substitutions is given by a list of pairs of terms \funf_{j}([(*x*)\vec]),\fung_{j}( [(*x*)\vec]):\typeY_{j}. A substitution**a**= [[(*x*)\vec]: = [(*a*)\vec]] has equal composites with them iff it is a,*unifier**ie*\funf_{j}[[(*x*)\vec]: = [(*a*)\vec]] = \fung_{j}[[(*x*)\vec]: = [(*a*)\vec]], or, in the informal notation, \funf_{j}([(*a*)\vec]) = \fung_{j}([(*a*)\vec]). The equaliser, if any, is the(Remark 1.7.8), since any other unifier is a substitute. Similarly pullbacks solve \funf*most general unifier*_{j}([(*x*)\vec]) = \fung_{j}([(*y*)\vec]). In Section 6.5 we shall construct the most general unifier in the simplest case, a free algebraic theory. **(c)**- A pullback rooted at the terminal object
*Z*= 1 is a product. In any category with binary products, pullbacks may be constructed from equalisers and*vice versa*(*cf*Remark 5.2.3).

EXAMPLES 5.1.4 Pullbacks of sets and functions have several names.

**(a)**- The equaliser of two parallel functions
*f*,*g*:*X*\rightrightarrows*Y*is (the inclusion of) the subset*E*= {*x*|*f*(*x*) =*g*(*x*)}. If*a*: G®*X*with*fo**a*=*go**a*then the results of*a*at all elements of G lie in*E*Ì*X*, so*a*restricts to*h*:G®*E*Ì*X*. **(b)**- The pullback of any two functions
*f*:*X*®*Z*and*g*:*Y*®*Z*is the subset {*x*,*y*|*f*(*x*) =*g*(*y*)} with the usual projections. A pair of maps from G gives rise to a map*a*,*b*:G®*Xx**Y*to the product, which restricts to the pullback in the same way as for the equaliser. **(c)**- If
*g*:*Y*Ì*Z*is a subset inclusion then the pullback is the inverse image,*f*^{-1}[*Y*] Ì*X*. **(d)**- If
*f*and*g*are both subset inclusions then the pullback,*X*Ç*Y*Ì*Z*, is their intersection (Example 2.1.6(d)).

EXAMPLES 5.1.5 Some other familiar semantic categories.

**(a)**- The restriction of the order on the source gives the equaliser
and on the product gives the pullback in
**Preord**,**Pos**,**CSLat**,**SLat**,**Lat**,**DLat**,**BA**,**Frm**,**HSL**,**Heyt**and**Dcpo**. This fails, however, in many popular categories of domains. **(b)**- Equalisers and pullbacks in
**Set**^{Cop}are constructed pointwise and the Yoneda embedding (Theorem 4.8.12(b)) \H_{(-)}:*C*\hookrightarrow**Set**^{Cop}preserves whatever limits exist. **(c)**- The category
**Mod**(*L*) of models of any algebraic theory*L*has pullbacks and equalisers. Indeed the forgetful functor**Mod**(*L*)®**Set**^{S}creates limits (*cf*Definition 4.5.10(c)), S being the set of sorts. **(d)**- The category of trichotomous orders (Definition
3.1.3) and
*strictly*monotone functions does not have products, but it has got pullbacks and equalisers, constructed in**Set**. This is because its maps are all injective, so pullbacks are intersections. **(e)**- A
is a set*coherence space**X*with two*symmetric*relations \coh (joined or coherent) and \icoh (un-joined or incoherent ) satisfying a trichotomy law: exactly one of*x*\coh*y*,*x*=*y*and*x*\icoh*y*holds. Anis a function which preserves all three relations, whence it also reflects them and is injective, so pullbacks are intersections.*embedding* **(f)**- The category of fields also has pullbacks and equalisers but
not binary products or a terminal object. We can say that two elements
*x*,*y*Î*K*of a field are*apart*in a*positive*sense which is preserved by homomorphisms, if $*z*.(*x*-*y*)*z*= 1, which we write as*x*#*y*. This obeys the*di*chotomy law that exactly one of*x*=*y*and*x*#*y*holds, whence all homomorphisms are injective. The full subcategory consisting of those fields in which a particular polynomial has a root (say*x*^{2}+1 = 0) has pullbacks but not equalisers.

EXAMPLES 5.1.6 Some squares which are ``spontaneous'' pullbacks.

**(a)**- Exercise 4.34 showed that the Church-
Rosser Theorem (Fact 2.3.3) may be expressed
as a commutative square in a certain category. This square is in fact a
pushout (a pullback in the opposite category) [
Bar81, Exercise 12.4.4].
**(b)**- The effect of the product functor on morphisms (Proposition
4.5.13) gives rise to pullback squares.
These also occurred in the diagrams Example
4.6.3(f) and Definition
4.7.9.
**(c)**- Let
**f**:*X*¢®*X*in*C*and**g**:*E*¢®*E*in G be maps in any two categories. Then this square (Proposition 4.8.3(c)) is a pullback: omitted diagram environment This means that the result of applying a pullback-preserving functor*P*:G*x**C*®*D*to this square yields another pullback:*cf*Exercises 3.20 and 5.9.

**Slices **
Pullbacks arise in three important ways in type theory:

**(a)**- they generalise products (so are also called
),*fibred products* **(b)**- they have something to do with equality, and
**(c)**- in Chapter VIII their primary role is
substitution,
*cf*Exercise 5.6.

In the first two cases there is a symmetry between the two legs, but this is
not true of substitution, where one is definitely acting on the other and
not *vice versa* . Let's look at (b) and then (c).

REMARK 5.1.7
The pullbacks below are in a sense trivial, in that the pullback of an identity
must be an isomorphism. But if we think of the pullback as a subset
*X*×_{Z}*Y* Ì *XxY*, on the left we obtain the ** graph of a function**,

omitted diagram environment

The even simpler case on the right gives the binary ** equality relation**,
( =

To see pullbacks as products exactly, we need to formalise the idea used in Lemma 4.5.16. For the terminal object, see Exercise 5.4.

DEFINITION 5.1.8
Let *X* be any object of any category *S*. The *slice category**S*¯ *X* has

**(a)**- as
*objects*the*S*-morphisms**d**:*Y*®*X*, **(b)**- as
*morphisms*the commuting triangles in*S*, omitted diagram environment **(c)**- and as
*identity*and*composition*those for*S*.

PROPOSITION 5.1.9
If *S* has chosen pullbacks against **u**:*X*¢® *X* then
**u**^{*}:*S*¯ *X*® *S*¯ *X*¢ is a functor.
This is a contravariant action (Section 4.2), except
that *id*^{*} need only be *isomorphic* to the identity
and (**u**;|)^{*} to **u**^{*}·|^{*}.

omitted diagram environment

PROOF: The effect of **u**^{*} on the morphism **f** is
the mediator between the pullback parallelograms. Identities and composites
are preserved by the same argument by uniqueness of mediators as in Proposition
4.5.13. []

The analogue of the slice for posets is just the lower set generated by an element
(Definition 3.1.7). In the next section we
shall use the same construction, but with the **d**s restricted to be
monos. It will appear in a more general form in Definition
8.3.8, where the **d**s belong to a specified
class but **u** and **f** will be arbitrary. An important common
generalisation of pullbacks and slices (comma categories) is given in Definition
7.3.8.