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 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 $\Sigma$ -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 coproduct type $A+B$ , which is “presented” by the injections ${\mathsf{inl}}:A\to A+B$ and ${\mathsf{inr}}:B\to A+B$ . Intuitively, we expect that $A+B$ contains exact copies of $A$ and $B$ disjointly, so that we should have

$\displaystyle{({\mathsf{inl}}(a_{1})={\mathsf{inl}}(a_{2}))}$	$\displaystyle\simeq{(a_{1}=a_{2})}$	(2.12.1)
$\displaystyle{({\mathsf{inr}}(b_{1})={\mathsf{inr}}(b_{2}))}$	$\displaystyle\simeq{(b_{1}=b_{2})}$	(2.12.2)
$\displaystyle{({\mathsf{inl}}(a)={\mathsf{inr}}(b))}$	$\displaystyle\simeq{\mathbf{0}}.$	(2.12.3)

We prove this as follows. Fix an element $a_{0}:A$ ; we will characterize the type family

(x\mapsto({\mathsf{inl}}(a_{0})=x)):A+B\to\mathcal{U}.

(2.12.4)

A similar argument would characterize the analogous family $x\mapsto(x={\mathsf{inr}}(b_{0}))$ for any $b_{0}:B$ . Together, these characterizations imply (2.12.1)–(2.12.3).

In order to characterize (2.12.4), we will define a type family $\mathsf{code}:A+B\to\mathcal{U}$ and show that $\mathchoice{\prod_{x:A+B}\,}{\mathchoice{{\textstyle\prod_{(x:A+B)}}}{\prod_{(% x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{\textstyle\prod_{(x:A% +B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{% \textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}% }(({\mathsf{inl}}(a_{0})=x)\simeq\mathsf{code}(x))$ . Since we want to conclude (2.12.1) from this, we should have $\mathsf{code}({\mathsf{inl}}(a))=(a_{0}=a)$ , and since we also want to conclude (2.12.3), we should have $\mathsf{code}({\mathsf{inr}}(b))=\mathbf{0}$ . The essential insight is that we can use the recursion principle of $A+B$ to define $\mathsf{code}:A+B\to\mathcal{U}$ by these two equations:

	$\displaystyle\mathsf{code}({\mathsf{inl}}(a))$	$\displaystyle:\!\!\equiv(a_{0}=a),$
	$\displaystyle\mathsf{code}({\mathsf{inr}}(b))$	$\displaystyle:\!\!\equiv\mathbf{0}.$

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 $({\mathsf{inl}}(a_{0})=x)\simeq\mathsf{code}(x)$ .

Proof.

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

\mathsf{encode}:\mathchoice{\prod_{(x:A+B)}\,}{\mathchoice{{\textstyle\prod_{(% x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{% \textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}% }{\mathchoice{{\textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{% \prod_{(x:A+B)}}}\mathchoice{\prod_{(p:{\mathsf{inl}}(a_{0})=x)}\,}{% \mathchoice{{\textstyle\prod_{(p:{\mathsf{inl}}(a_{0})=x)}}}{\prod_{(p:{% \mathsf{inl}}(a_{0})=x)}}{\prod_{(p:{\mathsf{inl}}(a_{0})=x)}}{\prod_{(p:{% \mathsf{inl}}(a_{0})=x)}}}{\mathchoice{{\textstyle\prod_{(p:{\mathsf{inl}}(a_{% 0})=x)}}}{\prod_{(p:{\mathsf{inl}}(a_{0})=x)}}{\prod_{(p:{\mathsf{inl}}(a_{0})% =x)}}{\prod_{(p:{\mathsf{inl}}(a_{0})=x)}}}{\mathchoice{{\textstyle\prod_{(p:{% \mathsf{inl}}(a_{0})=x)}}}{\prod_{(p:{\mathsf{inl}}(a_{0})=x)}}{\prod_{(p:{% \mathsf{inl}}(a_{0})=x)}}{\prod_{(p:{\mathsf{inl}}(a_{0})=x)}}}\mathsf{code}(x)

by transporting reflexivity along $p$ :

\mathsf{encode}(x,p):\!\!\equiv\mathsf{transport}^{\mathsf{code}}(p,\mathsf{% refl}_{a_{0}}).

Note that $\mathsf{refl}_{a_{0}}:\mathsf{code}({\mathsf{inl}}(a_{0}))$ , since $\mathsf{code}({\mathsf{inl}}(a_{0}))\equiv(a_{0}=a_{0})$ by definition of $\mathsf{code}$ . Next, we define a function

\mathsf{decode}:\mathchoice{\prod_{(x:A+B)}\,}{\mathchoice{{\textstyle\prod_{(% x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{% \textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}% }{\mathchoice{{\textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{% \prod_{(x:A+B)}}}\mathchoice{\prod_{(c:\mathsf{code}(x))}\,}{\mathchoice{{% \textstyle\prod_{(c:\mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{% (c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}}{\mathchoice{{\textstyle% \prod_{(c:\mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf% {code}(x))}}{\prod_{(c:\mathsf{code}(x))}}}{\mathchoice{{\textstyle\prod_{(c:% \mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))% }}{\prod_{(c:\mathsf{code}(x))}}}({\mathsf{inl}}(a_{0})=x).

To define $\mathsf{decode}(x,c)$ , we may first use the elimination principle of $A+B$ to divide into cases based on whether $x$ is of the form ${\mathsf{inl}}(a)$ or the form ${\mathsf{inr}}(b)$ .

In the first case, where $x\equiv{\mathsf{inl}}(a)$ , then $\mathsf{code}(x)\equiv(a_{0}=a)$ , so that $c$ is an identification between $a_{0}$ and $a$ . Thus, $\mathsf{ap}_{{\mathsf{inl}}}(c):({\mathsf{inl}}(a_{0})={\mathsf{inl}}(a))$ so we can define this to be $\mathsf{decode}({\mathsf{inl}}(a),c)$ .

In the second case, where $x\equiv{\mathsf{inr}}(b)$ , then $\mathsf{code}(x)\equiv\mathbf{0}$ , so that $c$ inhabits the empty type. Thus, the elimination rule of $\mathbf{0}$ yields a value for $\mathsf{decode}({\mathsf{inr}}(b),c)$ .

This completes the definition of $\mathsf{decode}$ ; we now show that $\mathsf{encode}(x,{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}})$ and $\mathsf{decode}(x,{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}})$ are quasi-inverses for all $x$ . On the one hand, suppose given $x:A+B$ and $p:{\mathsf{inl}}(a_{0})=x$ ; we want to show $\mathsf{decode}(x,\mathsf{encode}(x,p))=p.$ But now by (based) path induction, it suffices to consider $x\equiv{\mathsf{inl}}(a_{0})$ and $p\equiv\mathsf{refl}_{{\mathsf{inl}}(a_{0})}$ :

	$\displaystyle\mathsf{decode}(x,\mathsf{encode}(x,p))$	$\displaystyle\equiv\mathsf{decode}({\mathsf{inl}}(a_{0}),\mathsf{encode}({% \mathsf{inl}}(a_{0}),\mathsf{refl}_{{\mathsf{inl}}(a_{0})}))$
		$\displaystyle\equiv\mathsf{decode}({\mathsf{inl}}(a_{0}),\mathsf{transport}^{% \mathsf{code}}(\mathsf{refl}_{{\mathsf{inl}}(a_{0})},\mathsf{refl}_{a_{0}}))$
		$\displaystyle\equiv\mathsf{decode}({\mathsf{inl}}(a_{0}),\mathsf{refl}_{a_{0}})$
		$\displaystyle\equiv{{\mathsf{inl}}}\mathopen{}\left({\mathsf{refl}_{a_{0}}}% \right)\mathclose{}$
		$\displaystyle\equiv\mathsf{refl}_{{\mathsf{inl}}(a_{0})}$
		$\displaystyle\equiv p.$

On the other hand, let $x:A+B$ and $c:\mathsf{code}(x)$ ; we want to show $\mathsf{encode}(x,\mathsf{decode}(x,c))=c$ . We may again divide into cases based on $x$ . If $x\equiv{\mathsf{inl}}(a)$ , then $c:a_{0}=a$ and $\mathsf{decode}(x,c)\equiv\mathsf{ap}_{{\mathsf{inl}}}(c)$ , so that

$\displaystyle\mathsf{encode}(x,\mathsf{decode}(x,c))$	$\displaystyle\equiv\mathsf{transport}^{\mathsf{code}}(\mathsf{ap}_{{\mathsf{% inl}}}(c),\mathsf{refl}_{a_{0}})$
	$\displaystyle=\mathsf{transport}^{a\mapsto(a_{0}=a)}(c,\mathsf{refl}_{a_{0}}){}$	(by Lemma 7 (http://planetmath.org/23typefamiliesarefibrationshmlem7))
	$\displaystyle=\mathsf{refl}_{a_{0}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}c{}$	(by Lemma 1 (http://planetmath.org/211identitytypehmlem1))
	$\displaystyle=c.$

Finally, if $x\equiv{\mathsf{inr}}(b)$ , then $c:\mathbf{0}$ , so we may conclude anything we wish. ∎

Of course, there is a corresponding theorem if we fix $b_{0}:B$ instead of $a_{0}:A$ .

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

\mathsf{encode}(a,{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}):({\mathsf{inl% }}(a_{0})={\mathsf{inl}}(a))\to(a_{0}=a)

and

\mathsf{encode}(b,{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}):({\mathsf{inl% }}(a_{0})={\mathsf{inr}}(b))\to\mathbf{0}.

The second of these states “ ${\mathsf{inl}}(a_{0})$ is not equal to ${\mathsf{inr}}(b)$ ”, i.e. the images of ${\mathsf{inl}}$ and ${\mathsf{inr}}$ are disjoint. The traditional reading of the first one, where identity types are viewed as propositions, is just injectivity of ${\mathsf{inl}}$ . The full homotopical statement of Theorem 1.12.5 (http://planetmath.org/212coproducts#Thmprethm1) gives more information: the types ${\mathsf{inl}}(a_{0})={\mathsf{inl}}(a)$ and $a_{0}=a$ are actually equivalent, as are ${\mathsf{inr}}(b_{0})={\mathsf{inr}}(b)$ and $b_{0}=b$ .

Remark 2.12.6.

In particular, since the two-element type $\mathbf{2}$ is equivalent to $\mathbf{1}+\mathbf{1}$ , we have ${0_{\mathbf{2}}}\neq{1_{\mathbf{2}}}$ .

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 “ $\mathsf{code}$ ” 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 $\mathsf{decode}$ generally for all instances of the fibration (i.e. as a function $\mathchoice{\prod_{x:A+B}\,}{\mathchoice{{\textstyle\prod_{(x:A+B)}}}{\prod_{(% x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{\textstyle\prod_{(x:A% +B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{% \textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}% }\mathsf{code}(x)\to({\mathsf{inl}}(a_{0})=x)$ ), so that path induction can be used to analyze $\mathsf{decode}(x,\mathsf{encode}(x,p))$ .

As usual, we can also characterize the action of transport in coproduct types. Given a type $X$ , a path $p:x_{1}=_{X}x_{2}$ , and type families $A,B:X\to\mathcal{U}$ , we have

	$\displaystyle\mathsf{transport}^{A+B}(p,{\mathsf{inl}}(a))$	$\displaystyle={\mathsf{inl}}(\mathsf{transport}^{A}(p,a)),$
	$\displaystyle\mathsf{transport}^{A+B}(p,{\mathsf{inr}}(b))$	$\displaystyle={\mathsf{inr}}(\mathsf{transport}^{B}(p,b)),$

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

Title	2.12 Coproducts
\metatable