2.8 The unit type

Trivial cases are sometimes important, so we mention briefly the case of the unit type 𝟏.

Theorem 2.8.1.

For any x,y:1, we have (x=y)≃1.


A functionMathworldPlanetmath (x=y)β†’πŸ is easy to define by sending everything to ⋆. Conversely, for any x,y:𝟏 we may assume by inductionMathworldPlanetmath that x≑⋆≑y. In this case we have 𝗋𝖾𝖿𝗅⋆:x=y, yielding a constant functionMathworldPlanetmath πŸβ†’(x=y).

To show that these are inversesPlanetmathPlanetmathPlanetmath, consider first an element u:𝟏. We may assume that u≑⋆, but this is also the result of the composite πŸβ†’(x=y)β†’πŸ.

On the other hand, suppose given p:x=y. By path induction, we may assume x≑y and p is 𝗋𝖾𝖿𝗅x. We may then assume that x is ⋆, in which case the composite (x=y)β†’πŸβ†’(x=y) takes p to 𝗋𝖾𝖿𝗅x, i.e.Β toΒ p. ∎

In particular, any two elements of 𝟏 are equal. We leave it to the reader to formulate this equivalence in terms of introduction, elimination, computation, and uniqueness rules. The transport lemma for 𝟏 is simply the transport lemma for constant type families (Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrations#Thmlem4)).

Title 2.8 The unit type