4.8 The object classifier
In type theory we have a basic notion of family of types, namely a function . We have seen that such families behave somewhat like fibrations in homotopy theory, with the fibration being the projection . A basic fact in homotopy theory is that every map is equivalent to a fibration. With univalence at our disposal, we can prove the same thing in type theory.
For any type family , the fiber of over is equivalent to :
using the left universal property of identity types. ∎
For any function , we have .
using the fact that is contractible. ∎
For any type there is an equivalence
We define by , and by . Now we have to verify that and that .
Let . By Lemma 4.8.1 (http://planetmath.org/48theobjectclassifier#Thmprelem1), for any , so it follows immediately that .
Let be a function. We have to find a path
First note that by Lemma 4.8.2 (http://planetmath.org/48theobjectclassifier#Thmprelem2), we have with and . By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), it remains to show . But by the computation rule for univalence and (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#S0.E3), we have , and the definition of immediately yields .∎
In particular, this implies that we have an object classifier in the sense of higher topos theory. Recall from Definition 2.1.7 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn1) that denotes the type of pointed types.
Let be a function. Then the diagram
is a pullback square (see http://planetmath.org/node/87642Exercise 2.11). Here the function is defined by
Note that we have the equivalences
which gives us a composite equivalence . We may display the action of this composite equivalence step by step by
Therefore, we get homotopies and . ∎
|Title||4.8 The object classifier|