2.15 Universal properties


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

(XA×B)(XA)×(XB) (2.15.1)

defined by f(𝗉𝗋1f,𝗉𝗋2f).

Theorem 2.15.2.

(2.15.1) is an equivalence.

Proof.

We define the quasi-inversePlanetmathPlanetmath by sending (g,h) to λx.(g(x),h(x)). (Technically, we have used the inductionMathworldPlanetmath principle for the cartesian productMathworldPlanetmath (XA)×(XB), to reduce to the case of a pair. From now on we will often apply this principle without explicit mention.)

Now given f:XA×B, the round-trip composite yields the function

λx.(𝗉𝗋1(f(x)),𝗉𝗋2(f(x))). (2.15.3)

By Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1), for any x:X we have (𝗉𝗋1(f(x)),𝗉𝗋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 (λx.g(x),λ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𝒰. Then we have a function

(x:X(A(x)×B(x)))(x:XA(x))×(x:XB(x)) (2.15.4)

defined as before by f(𝗉𝗋1f,𝗉𝗋2f).

Theorem 2.15.5.

(2.15.4) is an equivalence.

Proof.

Left to the reader. ∎

Just as Σ-types are a generalizationPlanetmathPlanetmath 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𝒰 and P:(x:X)A(x)𝒰. Then we have a function

(x:X(a:A(x))P(x,a))((g:(x:X)A(x))(x:X)P(x,g(x))). (2.15.6)

Note that if we have P(x,a):B(x) for some B:X𝒰, 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 λx.(g(x),h(x)). Now given f:(x:X)(a:A(x))P(x,a), the round-trip composite yields the function

λx.(𝗉𝗋1(f(x)),𝗉𝗋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 Σ-types) we have

(𝗉𝗋1(f(x)),𝗉𝗋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 (λx.g(x),λx.h(x)), which is judgmentally equal to (g,h) as before. ∎

This is noteworthy because the propositions-as-types interpretationMathworldPlanetmathPlanetmath of (2.15.6) is “the axiom of choiceMathworldPlanetmath”. If we read Σ as “there exists” and Π (sometimes) as “for all”, we can pronounce:

  • (x:X)(a:A(x))P(x,a) as “for all x:X there exists an a:A(x) such that P(x,a)”, and

  • (g:(x:X)A(x))(x:X)P(x,g(x)) as “there exists a choice function g:(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 antecedentPlanetmathPlanetmathPlanetmath is actually equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to its conclusionMathworldPlanetmath. (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 productsPlanetmathPlanetmathPlanetmathPlanetmath. 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 expresses the cartesian closureMathworldPlanetmathPlanetmath adjunctionPlanetmathPlanetmath:

((A×B)C)(A(BC)).

The dependent version of this is formulated for a type family C:A×B𝒰:

(w:A×BC(w))((x:A)(y:B)C(x,y)).

Here the right-to-left function is simply the induction principle for A×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 Σ-types:

(w:(x:A)B(x)C(w))((x:A)(y:B(x))C(x,y)). (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:

((x:A)(p:a=x)B(x,p))B(a,𝗋𝖾𝖿𝗅a) (2.15.10)

for any a:A and type family B:(x:A)(a=x)𝒰. However, inductive types with recursion, such as the natural numbersMathworldPlanetmath, 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 colimitsMathworldPlanetmath of types. In http://planetmath.org/node/87640Exercise 2.9 we ask the reader to show that the coproductMathworldPlanetmath type A+B also has the expected universal property, and the nullary cases of 𝟏 (the terminal objectMathworldPlanetmath) and 𝟎 (the initial object) are easy.

For pullbacksPlanetmathPlanetmath, the expected explicit construction works: given f:AC and g:BC, we define

A×CB:(a:A)(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.

Title 2.15 Universal properties
\metatable