Let $\webleft (X,x_{0}\webright )$, $\webleft (Y,y_{0}\webright )$, $\webleft (Z,z_{0}\webright )$, and $\webleft (A,a_{0}\webright )$ be pointed sets.
-
Functoriality. The assignment $\webleft (X,Y,Z,f,g\webright )\mapsto X\times _{f,Z,g}Y$ 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 morphism of pointed sets
\[ \xi \colon \webleft (X\times _{Z}Y,\webleft (x_{0},y_{0}\webright )\webright )\overset {\exists !}{\to }\webleft (X'\times _{Z'}Y',\webleft (x'_{0},y'_{0}\webright )\webright ) \]given by
\[ \xi \webleft (x,y\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\phi \webleft (x\webright ),\psi \webleft (y\webright )\webright ) \]for each $\webleft (x,y\webright )\in X\times _{Z}Y$, which is the unique morphism of pointed sets making the diagram
commute.
-
Associativity. Given a diagram
in $\mathsf{Sets}_{*}$, we have isomorphisms of pointed sets
\[ \webleft (X\times _{W}Y\webright )\times _{V}Z\cong \webleft (X\times _{W}Y\webright )\times _{Y}\webleft (Y\times _{V}Z\webright ) \cong X\times _{W}\webleft (Y\times _{V}Z\webright ), \]where these pullbacks are built as in the diagrams
-
Unitality. We have isomorphisms of pointed sets
-
Commutativity. We have an isomorphism of pointed sets
-
Interaction With Products. We have an isomorphism of pointed sets
- Symmetric Monoidality. The triple $\webleft (\mathsf{Sets}_{*},\times _{X},X\webright )$ is a symmetric monoidal category.
