Let $A$, $B$, $C$, and $X$ be sets.
-
Functoriality. The assignment $\webleft (A,B,C,f,g\webright )\mapsto A\times _{f,C,g}B$ defines a functor
\[ -_{1}\times _{-_{3}}-_{1}\colon \mathsf{Fun}\webleft (\mathcal{P},\mathsf{Sets}\webright )\to \mathsf{Sets}, \]
where $\mathcal{P}$ is the category that looks like this:
In particular, the action on morphisms of $-_{1}\times _{-_{3}}-_{1}$ is given by sending a morphism
in $\mathsf{Fun}\webleft (\mathcal{P},\mathsf{Sets}\webright )$ to the map $\xi \colon A\times _{C}B\overset {\exists !}{\to }A'\times _{C'}B'$ given by
\[ \xi \webleft (a,b\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\phi \webleft (a\webright ),\psi \webleft (b\webright )\webright ) \]for each $\webleft (a,b\webright )\in A\times _{C}B$, which is the unique map making the diagram
commute.
-
Associativity. Given a diagram
in $\mathsf{Sets}$, we have isomorphisms of sets
\[ \webleft (A\times _{X}B\webright )\times _{Y}C\cong \webleft (A\times _{X}B\webright )\times _{B}\webleft (B\times _{Y}C\webright ) \cong A\times _{X}\webleft (B\times _{Y}C\webright ), \]where these pullbacks are built as in the diagrams
-
Unitality. We have isomorphisms of sets
-
Commutativity. We have an isomorphism of sets
-
Annihilation With the Empty Set. We have isomorphisms of sets
-
Interaction With Products. We have an isomorphism of sets
- Symmetric Monoidality. The triple $\webleft (\mathsf{Sets},\times _{X},X\webright )$ is a symmetric monoidal category.
