So far, most of the type formers we have considered have been what are called negative. Intuitively, this means that their elements are determined by their behavior under the elimination rules: a (dependent) pair is determined by its projections, and a (dependent) function is determined by its values. The identity types of negative types can almost always be characterized straightforwardly, along with all of their higher structure, as we have done in §2.6 (http://planetmath.org/26cartesianproducttypes) to §2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom). The universe is not exactly a negative type, but its identity types behave similarly: we have a straightforward characterization (univalence) and a description of the higher structure. Identity types themselves, of course, are a special case.
We now consider our first example of a positive type former. Again informally, a positive type is one which is “presented” by certain constructors, with the universal property of a presentation being expressed by its elimination rule. (Categorically speaking, a positive type has a “mapping out” universal property, while a negative type has a “mapping in” universal property.) Because computing with presentations is, in general, an uncomputable problem, for positive types we cannot always expect a straightforward characterization of the identity type. However, in many particular cases, a characterization or partial characterization does exist, and can be obtained by the general method that we introduce with this example.
(Technically, our chosen presentation of cartesian products and -types is also positive. However, because these types also admit a negative presentation which differs only slightly, their identity types have a direct characterization that does not require the method to be described here.)
We prove this as follows. Fix an element ; we will characterize the type family
In order to characterize (2.12.4), we will define a type family and show that . Since we want to conclude (2.12.1) from this, we should have , and since we also want to conclude (2.12.3), we should have . The essential insight is that we can use the recursion principle of to define by these two equations:
This is a very simple example of a proof technique that is used quite a bit when doing homotopy theory in homotopy type theory; see e.g. §8.1 (http://planetmath.org/81pi1s1),§8.9 (http://planetmath.org/89ageneralstatementoftheencodedecodemethod). We can now show:
For all we have .
The key to the following proof is that we do it for all points together, enabling us to use the elimination principle for the coproduct. We first define a function
by transporting reflexivity along :
Note that , since by definition of . Next, we define a function
To define , we may first use the elimination principle of to divide into cases based on whether is of the form or the form .
In the first case, where , then , so that is an identification between and . Thus, so we can define this to be .
In the second case, where , then , so that inhabits the empty type. Thus, the elimination rule of yields a value for .
This completes the definition of ; we now show that and are quasi-inverses for all . On the one hand, suppose given and ; we want to show But now by (based) path induction, it suffices to consider and :
On the other hand, let and ; we want to show . We may again divide into cases based on . If , then and , so that
|(by Lemma 7 (http://planetmath.org/23typefamiliesarefibrationshmlem7))|
|(by Lemma 1 (http://planetmath.org/211identitytypehmlem1))|
Finally, if , then , so we may conclude anything we wish. ∎
Of course, there is a corresponding theorem if we fix instead of .
In particular, Theorem 2.12.5 (http://planetmath.org/212coproducts#Thmprethm1) implies that for any and there are functions
The second of these states “ is not equal to ”, i.e. the images of and are disjoint. The traditional reading of the first one, where identity types are viewed as propositions, is just injectivity of . The full homotopical statement of Theorem 1.12.5 (http://planetmath.org/212coproducts#Thmprethm1) gives more information: the types and are actually equivalent, as are and .
In particular, since the two-element type is equivalent to , we have .
This proof illustrates a general method for describing path spaces, which we will use often. To characterize a path space, the first step is to define a comparison fibration “” that provides a more explicit description of the paths. There are several different methods for proving that such a comparison fibration is equivalent to the paths (we show a few different proofs of the same result in §8.1 (http://planetmath.org/81pi1s1)). The one we have used here is called the encode-decode method: the key idea is to define generally for all instances of the fibration (i.e. as a function ), so that path induction can be used to analyze .
As usual, we can also characterize the action of transport in coproduct types. Given a type , a path , and type families , we have
where as usual, in the superscript denotes abusively the type family . The proof is an easy path induction.