2.15 Universal properties

By combining the path computation rules described in the preceding sections, we can show that various type forming operations satisfy the expected universal properties, interpreted in a homotopical way as equivalences.For instance, given types $X,A,B$, we have a function

$$(X\to A\times B)\to (X\to A)\times (X\to B)$$(2.15.1)

defined by $f\mapsto ({\mathrm{𝗉𝗋}}_1\circ f,{\mathrm{𝗉𝗋}}_2\circ f)$.

Theorem 2.15.2.

(2.15.1) is an equivalence.

Proof.

We define the quasi-inverse by sending $(g,h)$ to $\lambda x.(g(x),h(x))$.(Technically, we have used the induction principle for the cartesian product $(X\to A)\times (X\to B)$, to reduce to the case of a pair.From now on we will often apply this principle without explicit mention.)

Now given $f:X\to A\times B$, the round-trip composite yields the function

$$\lambda x.({\mathrm{𝗉𝗋}}_1(f(x)),{\mathrm{𝗉𝗋}}_2(f(x))).$$(2.15.3)

By Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1), for any $x:X$ we have $({\mathrm{𝗉𝗋}}_1(f(x)),{\mathrm{𝗉𝗋}}_2(f(x)))=f(x)$.Thus, by function extensionality, the function (2.15.3) is equal to $f$.

On the other hand, given $(g,h)$, the round-trip composite yields the pair $(\lambda x.g(x),\lambda x.h(x))$.By the uniqueness principle for functions, this is (judgmentally) equal to $(g,h)$.∎

In fact, we also have a dependently typed version of this universal property.Suppose given a type $X$ and type families $A,B:X\to 𝒰$.Then we have a function

$$\left(\prod _{x:X}(A(x)\times B(x))\right)\to \left(\prod _{x:X}A(x)\right)\times \left(\prod _{x:X}B(x)\right)$$(2.15.4)

defined as before by $f\mapsto ({\mathrm{𝗉𝗋}}_1\circ f,{\mathrm{𝗉𝗋}}_2\circ f)$.

Theorem 2.15.5.

(2.15.4) is an equivalence.

Proof.

Left to the reader.∎

Just as $\mathrm{\Sigma }$-types are a generalization of cartesian products, they satisfy a generalized version of this universal property.Jumping right to the dependently typed version, suppose we have a type $X$ and type families $A:X\to 𝒰$ and $P:{\prod }_{(x:X)}A(x)\to 𝒰$.Then we have a function

$$\left(\prod _{x:X}\sum _{(a:A(x))}P(x,a)\right)\to \left(\sum _{(g:{\prod }_{(x:X)}A(x))}\prod _{(x:X)}P(x,g(x))\right).$$(2.15.6)

Note that if we have $P(x,a):\equiv B(x)$ for some $B:X\to 𝒰$, then (2.15.6) reduces to (2.15.4).

Theorem 2.15.7.

(2.15.6) is an equivalence.

Proof.

As before, we define a quasi-inverse to send $(g,h)$ to the function $\lambda x.(g(x),h(x))$.Now given $f:{\prod }_{(x:X)}{\sum }_{(a:A(x))}P(x,a)$, the round-trip composite yields the function

$$\lambda x.({\mathrm{𝗉𝗋}}_1(f(x)),{\mathrm{𝗉𝗋}}_2(f(x))).$$(2.15.8)

Now for any $x:X$, by Corollary 2.7.3 (http://planetmath.org/27sigmatypes#Thmprecor1) (the uniqueness principle for $\mathrm{\Sigma }$-types) we have

$$({\mathrm{𝗉𝗋}}_1(f(x)),{\mathrm{𝗉𝗋}}_2(f(x)))=f(x).$$

Thus, by function extensionality, (2.15.8) is equal to $f$.On the other hand, given $(g,h)$, the round-trip composite yields $(\lambda x.g(x),\lambda x.h(x))$, which is judgmentally equal to $(g,h)$ as before.∎

This is noteworthy because the propositions-as-types interpretation of (2.15.6) is “the axiom of choice”.If we read $\mathrm{\Sigma }$ as “there exists” and $\mathrm{\Pi }$ (sometimes) as “for all”, we can pronounce:

• ${\prod }_{(x:X)}{\sum }_{(a:A(x))}P(x,a)$ as “for all $x:X$ there exists an $a:A(x)$ such that $P(x,a)$”, and

• ${\sum }_{(g:{\prod }_{(x:X)}A(x))}{\prod }_{(x:X)}P(x,g(x))$ as “there exists a choice function $g:{\prod }_{(x:X)}A(x)$ such that for all $x:X$ we have $P(x,g(x))$”.

Thus, Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3) says that not only is the axiom of choice “true”, its antecedent is actually equivalent to its conclusion.(On the other hand, the classical mathematician may find that (2.15.6) does not carry the usual meaning of the axiom of choice, since we have already specified the values of $g$, and there are no choices left to be made.We will return to this point in §3.8 (http://planetmath.org/38theaxiomofchoice).)

The above universal property for pair types is for “mapping in”, which is familiar from the category-theoretic notion of products.However, pair types also have a universal property for “mapping out”, which may look less familiar.In the case of cartesian products, the non-dependent version simply expressesthe cartesian closure adjunction:

$$((A\times B)\to C)\simeq (A\to (B\to C)).$$

The dependent version of this is formulated for a type family $C:A\times B\to 𝒰$:

$$\left(\prod _{w:A\times B}C(w)\right)\simeq \left(\prod _{(x:A)}\prod _{(y:B)}C(x,y)\right).$$

Here the right-to-left function is simply the induction principle for $A\times B$, while the left-to-right is evaluation at a pair.We leave it to the reader to prove that these are quasi-inverses.There is also a version for $\mathrm{\Sigma }$-types:

$$\left(\prod _{w:{\sum }_{(x:A)}B(x)}C(w)\right)\simeq \left(\prod _{(x:A)}\prod _{(y:B(x))}C(x,y)\right).$$(2.15.9)

Again, the right-to-left function is the induction principle.

Some other induction principles are also part of universal properties of this sort.For instance, path induction is the right-to-left direction of an equivalence as follows:

$$\left(\prod _{(x:A)}\prod _{(p:a=x)}B(x,p)\right)\simeq B(a,{\mathrm{𝗋𝖾𝖿𝗅}}_a)$$(2.15.10)

for any $a:A$ and type family $B:{\prod }_{(x:A)}(a=x)\to 𝒰$.However, inductive types with recursion, such as the natural numbers, have more complicated universal properties; see http://planetmath.org/node/87578Chapter 5.

Since Theorem 2.15.2 (http://planetmath.org/215universalproperties#Thmprethm1) expresses the usual universal property of a cartesian product (in an appropriate homotopy-theoretic sense), the categorically inclined reader may well wonder about other limits and colimits of types.In http://planetmath.org/node/87640Exercise 2.9 we ask the reader to show that the coproduct type $A+B$ also has the expected universal property, and the nullary cases of $\mathrm{𝟏}$ (the terminal object) and $\mathrm{𝟎}$ (the initial object) are easy.

For pullbacks, the expected explicit construction works: given $f:A\to C$ and $g:B\to C$, we define

$$A{\times }_{C}B:\equiv \sum _{(a:A)}\sum _{(b:B)}(f(a)=g(b)).$$(2.15.11)

In http://planetmath.org/node/87642Exercise 2.11 we ask the reader to verify this.Some more general homotopy limits can be constructed in a similar way, but for colimits we will need a new ingredient; see http://planetmath.org/node/87579Chapter 6.