2.12 Coproducts

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 projectionsPlanetmathPlanetmath, 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 structureMathworldPlanetmath, as we have done in §2.6 (http://planetmath.org/26cartesianproducttypes) to §2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom). The universePlanetmathPlanetmath 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 propertyMathworldPlanetmath of a presentationMathworldPlanetmathPlanetmathPlanetmath 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 productsMathworldPlanetmath 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.)

Consider the coproductMathworldPlanetmath type A+B, which is “presented” by the injections 𝗂𝗇𝗅:AA+B and 𝗂𝗇𝗋:BA+B. Intuitively, we expect that A+B contains exact copies of A and B disjointly, so that we should have

(𝗂𝗇𝗅(a1)=𝗂𝗇𝗅(a2)) (a1=a2) (2.12.1)
(𝗂𝗇𝗋(b1)=𝗂𝗇𝗋(b2)) (b1=b2) (2.12.2)
(𝗂𝗇𝗅(a)=𝗂𝗇𝗋(b)) 𝟎. (2.12.3)

We prove this as follows. Fix an element a0:A; we will characterize the type family

(x(𝗂𝗇𝗅(a0)=x)):A+B𝒰. (2.12.4)

A similar argument would characterize the analogous family x(x=𝗂𝗇𝗋(b0)) for any b0:B. Together, these characterizations imply (2.12.1)–(2.12.3).

In order to characterize (2.12.4), we will define a type family 𝖼𝗈𝖽𝖾:A+B𝒰 and show that (x:A+B)((𝗂𝗇𝗅(a0)=x)𝖼𝗈𝖽𝖾(x)). Since we want to conclude (2.12.1) from this, we should have 𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(a))=(a0=a), and since we also want to conclude (2.12.3), we should have 𝖼𝗈𝖽𝖾(𝗂𝗇𝗋(b))=𝟎. The essential insight is that we can use the recursion principle of A+B to define 𝖼𝗈𝖽𝖾:A+B𝒰 by these two equations:

𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(a)) :(a0=a),
𝖼𝗈𝖽𝖾(𝗂𝗇𝗋(b)) :𝟎.

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:

Theorem 2.12.5.

For all x:A+B we have (inl(a0)=x)code(x).


The key to the following proof is that we do it for all points x together, enabling us to use the elimination principle for the coproduct. We first define a function


by transporting reflexivityMathworldPlanetmath along p:


Note that 𝗋𝖾𝖿𝗅a0:𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(a0)), since 𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(a0))(a0=a0) by definition of 𝖼𝗈𝖽𝖾. Next, we define a function


To define 𝖽𝖾𝖼𝗈𝖽𝖾(x,c), we may first use the elimination principle of A+B to divide into cases based on whether x is of the form 𝗂𝗇𝗅(a) or the form 𝗂𝗇𝗋(b).

In the first case, where x𝗂𝗇𝗅(a), then 𝖼𝗈𝖽𝖾(x)(a0=a), so that c is an identification between a0 and a. Thus, 𝖺𝗉𝗂𝗇𝗅(c):(𝗂𝗇𝗅(a0)=𝗂𝗇𝗅(a)) so we can define this to be 𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(a),c).

In the second case, where x𝗂𝗇𝗋(b), then 𝖼𝗈𝖽𝖾(x)𝟎, so that c inhabits the empty type. Thus, the elimination rule of 𝟎 yields a value for 𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗋(b),c).

This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the definition of 𝖽𝖾𝖼𝗈𝖽𝖾; we now show that 𝖾𝗇𝖼𝗈𝖽𝖾(x,) and 𝖽𝖾𝖼𝗈𝖽𝖾(x,) are quasi-inversesPlanetmathPlanetmath for all x. On the one hand, suppose given x:A+B and p:𝗂𝗇𝗅(a0)=x; we want to show 𝖽𝖾𝖼𝗈𝖽𝖾(x,𝖾𝗇𝖼𝗈𝖽𝖾(x,p))=p. But now by (based) path inductionMathworldPlanetmath, it suffices to consider x𝗂𝗇𝗅(a0) and p𝗋𝖾𝖿𝗅𝗂𝗇𝗅(a0):

𝖽𝖾𝖼𝗈𝖽𝖾(x,𝖾𝗇𝖼𝗈𝖽𝖾(x,p)) 𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(a0),𝖾𝗇𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(a0),𝗋𝖾𝖿𝗅𝗂𝗇𝗅(a0)))

On the other hand, let x:A+B and c:𝖼𝗈𝖽𝖾(x); we want to show 𝖾𝗇𝖼𝗈𝖽𝖾(x,𝖽𝖾𝖼𝗈𝖽𝖾(x,c))=c. We may again divide into cases based on x. If x𝗂𝗇𝗅(a), then c:a0=a and 𝖽𝖾𝖼𝗈𝖽𝖾(x,c)𝖺𝗉𝗂𝗇𝗅(c), so that

𝖾𝗇𝖼𝗈𝖽𝖾(x,𝖽𝖾𝖼𝗈𝖽𝖾(x,c)) 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝖽𝖾(𝖺𝗉𝗂𝗇𝗅(c),𝗋𝖾𝖿𝗅a0)
=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍a(a0=a)(c,𝗋𝖾𝖿𝗅a0) (by Lemma 7 (http://planetmath.org/23typefamiliesarefibrationshmlem7))
=𝗋𝖾𝖿𝗅a0\centerdotc (by Lemma 1 (http://planetmath.org/211identitytypehmlem1))

Finally, if x𝗂𝗇𝗋(b), then c:𝟎, so we may conclude anything we wish. ∎

Of course, there is a corresponding theorem if we fix b0:B instead of a0:A.

In particular, Theorem 2.12.5 (http://planetmath.org/212coproducts#Thmprethm1) implies that for any a:A and b:B there are functions




The second of these states “𝗂𝗇𝗅(a0) is not equal to 𝗂𝗇𝗋(b)”, i.e. the images of 𝗂𝗇𝗅 and 𝗂𝗇𝗋 are disjoint. The traditional reading of the first one, where identity types are viewed as propositionsPlanetmathPlanetmath, is just injectivity of 𝗂𝗇𝗅. The full homotopical statement of Theorem 1.12.5 (http://planetmath.org/212coproducts#Thmprethm1) gives more information: the types 𝗂𝗇𝗅(a0)=𝗂𝗇𝗅(a) and a0=a are actually equivalentMathworldPlanetmathPlanetmathPlanetmath, as are 𝗂𝗇𝗋(b0)=𝗂𝗇𝗋(b) and b0=b.

Remark 2.12.6.

In particular, since the two-element type 2 is equivalent to 1+1, we have 0212.

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 (x:A+B)𝖼𝗈𝖽𝖾(x)(𝗂𝗇𝗅(a0)=x)), so that path induction can be used to analyze 𝖽𝖾𝖼𝗈𝖽𝖾(x,𝖾𝗇𝖼𝗈𝖽𝖾(x,p)).

As usual, we can also characterize the action of transport in coproduct types. Given a type X, a path p:x1=Xx2, and type families A,B:X𝒰, we have

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍A+B(p,𝗂𝗇𝗅(a)) =𝗂𝗇𝗅(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍A(p,a)),
𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍A+B(p,𝗂𝗇𝗋(b)) =𝗂𝗇𝗋(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B(p,b)),

where as usual, A+B in the superscript denotes abusively the type family xA(x)+B(x). The proof is an easy path induction.

Title 2.12 Coproducts