2.8 The unit type
Trivial cases are sometimes important, so we mention briefly the case of the unit type .
For any , we have .
On the other hand, suppose given . By path induction, we may assume and is . We may then assume that is , in which case the composite takes to , i.e. to . ∎
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|