6.8 Pushouts

From a category-theoretic point of view, one of the important aspects of any foundational system is the ability to construct limits and colimits. In set-theoretic foundations, these are limits and colimits of sets, whereas in our case they are limits and colimits of types. We have seen in §2.15 (http://planetmath.org/215universalproperties) that cartesian product types have the correct universal property of a categorical product of types, and in http://planetmath.org/node/87640Exercise 2.9 that coproduct types likewise have their expected universal property.

As remarked in §2.15 (http://planetmath.org/215universalproperties), more general limits can be constructed using identity types and $\Sigma$ -types, e.g. the pullback of $f:A\to C$ and $g:B\to C$ is $\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}% }{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:% A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{% (a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice{\sum_{(b:B)}\,}{\mathchoice{{% \textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{% \mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}% }}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:% B)}}}(f(a)=g(b))$ (see http://planetmath.org/node/87642Exercise 2.11). However, more general colimits require identifying elements coming from different types, for which higher inductives are well-adapted. Since all our constructions are homotopy-invariant, all our colimits are necessarily homotopy colimits, but we drop the ubiquitous adjective in the interests of concision.

In this section we discuss pushouts, as perhaps the simplest and one of the most useful colimits. Indeed, one expects all finite colimits (for a suitable homotopical definition of “finite”) to be constructible from pushouts and finite coproducts. It is also possible to give a direct construction of more general colimits using higher inductive types, but this is somewhat technical, and also not completely satisfactory since we do not yet have a good fully general notion of homotopy coherent diagrams.

Suppose given a span of types and functions:

\includegraphics

HoTT_fig_6.8.1.png

The pushout of this span is the higher inductive type $A\sqcup^{C}B$ presented by

•

a function ${\mathsf{inl}}:A\to A\sqcup^{C}B$ ,
•

a function ${\mathsf{inr}}:B\to A\sqcup^{C}B$ , and
•

for each $c : C$ a path $\mathsf{glue}(c):({\mathsf{inl}}(f(c))={\mathsf{inr}}(g(c)))$ .

In other words, $A\sqcup^{C}B$ is the disjoint union of $A$ and $B$ , together with for every $c : C$ a witness that $f(c)$ and $g(c)$ are equal. The recursion principle says that if $D$ is another type, we can define a map $s:A\sqcup^{C}B\to{}D$ by defining

•

for each $a : A$ , the value of $s({\mathsf{inl}}(a)):D$ ,
•

for each $b : B$ , the value of $s({\mathsf{inr}}(b)):D$ , and
•

for each $c : C$ , the value of $\mathsf{ap}_{s}(\mathsf{glue}(c)):s({\mathsf{inl}}(f(c)))=s({\mathsf{inr}}(g(c% )))$ .

We leave it to the reader to formulate the induction principle. It also implies the uniqueness principle that if $s,s^{\prime}:A\sqcup^{C}B\to{}D$ are two maps such that

	$\displaystyle s({\mathsf{inl}}(a))$	$\displaystyle=s^{\prime}({\mathsf{inl}}(a))$
	$\displaystyle s({\mathsf{inr}}(b))$	$\displaystyle=s^{\prime}({\mathsf{inr}}(b))$
	$\displaystyle\mathsf{ap}_{s}(\mathsf{glue}(c))$	$\displaystyle=\mathsf{ap}_{s^{\prime}}(\mathsf{glue}(c))\qquad\text{(modulo % the previous two equalities)}$

for every $a, b, c$ , then $s=s^{\prime}$ .

To formulate the universal property of a pushout, we introduce the following.

Definition 6.8.1.

Given a span $\mathscr{D}=(A\xleftarrow{f}C\xrightarrow{g}B)$ and a type $D$ , a cocone under $\mathscr{D}$ with vertex $D$ consists of functions $i:A\to{}D$ and $j:B\to{}D$ and a homotopy $h:\mathchoice{\prod_{c:C}\,}{\mathchoice{{\textstyle\prod_{(c:C)}}}{\prod_{(c:% C)}}{\prod_{(c:C)}}{\prod_{(c:C)}}}{\mathchoice{{\textstyle\prod_{(c:C)}}}{% \prod_{(c:C)}}{\prod_{(c:C)}}{\prod_{(c:C)}}}{\mathchoice{{\textstyle\prod_{(c% :C)}}}{\prod_{(c:C)}}{\prod_{(c:C)}}{\prod_{(c:C)}}}(i(f(c))=j(g(c)))$ :

\includegraphics

HoTT_fig_6.8.2.png

We denote by $\mathsf{cocone}_{\mathscr{D}}(D)$ the type of all such cocones, i.e.

\mathsf{cocone}_{\mathscr{D}}(D):\!\!\equiv\mathchoice{\sum_{(i:A\to D)}\,}{% \mathchoice{{\textstyle\sum_{(i:A\to D)}}}{\sum_{(i:A\to D)}}{\sum_{(i:A\to D)% }}{\sum_{(i:A\to D)}}}{\mathchoice{{\textstyle\sum_{(i:A\to D)}}}{\sum_{(i:A% \to D)}}{\sum_{(i:A\to D)}}{\sum_{(i:A\to D)}}}{\mathchoice{{\textstyle\sum_{(% i:A\to D)}}}{\sum_{(i:A\to D)}}{\sum_{(i:A\to D)}}{\sum_{(i:A\to D)}}}% \mathchoice{\sum_{(j:B\to D)}\,}{\mathchoice{{\textstyle\sum_{(j:B\to D)}}}{% \sum_{(j:B\to D)}}{\sum_{(j:B\to D)}}{\sum_{(j:B\to D)}}}{\mathchoice{{% \textstyle\sum_{(j:B\to D)}}}{\sum_{(j:B\to D)}}{\sum_{(j:B\to D)}}{\sum_{(j:B% \to D)}}}{\mathchoice{{\textstyle\sum_{(j:B\to D)}}}{\sum_{(j:B\to D)}}{\sum_{% (j:B\to D)}}{\sum_{(j:B\to D)}}}\mathchoice{\prod_{(c:C)}\,}{\mathchoice{{% \textstyle\prod_{(c:C)}}}{\prod_{(c:C)}}{\prod_{(c:C)}}{\prod_{(c:C)}}}{% \mathchoice{{\textstyle\prod_{(c:C)}}}{\prod_{(c:C)}}{\prod_{(c:C)}}{\prod_{(c% :C)}}}{\mathchoice{{\textstyle\prod_{(c:C)}}}{\prod_{(c:C)}}{\prod_{(c:C)}}{% \prod_{(c:C)}}}(i(f(c))=j(g(c))).

Of course, there is a canonical cocone under $\mathscr{D}$ with vertex $A\sqcup^{C}B$ consisting of ${\mathsf{inl}}$ , ${\mathsf{inr}}$ , and $\mathsf{glue}$ .

\includegraphics

HoTT_fig_6.8.3.png

The following lemma says that this is the universal such cocone.

Lemma 6.8.2.

For any type $E$ , there is an equivalence

(A\sqcup^{C}B\to E)\;\simeq\;\mathsf{cocone}_{\mathscr{D}}(E).

Proof.

Let’s consider an arbitrary type $E:\mathcal{U}$ . There is a canonical function

\left\{\begin{array}[]{rcl}(A\sqcup^{C}B\to{}E)&\longrightarrow&\mathsf{cocone% }_{\mathscr{D}}(E)\\ t&\longmapsto&t\circ c_{\sqcup}\end{array}\right.

defined by sending $(i,j,h)$ to $(t\circ{}i,t\circ{}j,\mathsf{ap}_{t}\circ{}h)$ . We show that this is an equivalence.

Firstly, given a $c=(i,j,h):\mathsf{cocone}_{\mathscr{D}}(E)$ , we need to construct a map $\mathsf{s}(c)$ from $A\sqcup^{C}B$ to $E$ .

\includegraphics

HoTT_fig_6.8.4.png

The map $\mathsf{s}(c)$ is defined in the following way

	$\displaystyle\mathsf{s}(c)({\mathsf{inl}}(a))$	$\displaystyle:\!\!\equiv i(a),$
	$\displaystyle\mathsf{s}(c)({\mathsf{inr}}(b))$	$\displaystyle:\!\!\equiv j(b),$
	$\displaystyle\mathsf{ap}_{\mathsf{s}(c)}(\mathsf{glue}(x))$	$\displaystyle:=h(x).$

We have defined a map

\left\{\begin{array}[]{rcl}\mathsf{cocone}_{\mathscr{D}}(E)&\longrightarrow&(A% \sqcup^{B}C\to{}E)\\ c&\longmapsto&\mathsf{s}(c)\end{array}\right.

and we need to prove that this map is an inverse to $t\mapsto{}t\circ c_{\sqcup}$ . On the one hand, if $c=(i,j,h):\mathsf{cocone}_{\mathscr{D}}(E)$ , we have

	$\displaystyle\mathsf{s}(c)\circ c_{\sqcup}$	$\displaystyle=(\mathsf{s}(c)\circ{\mathsf{inl}},\mathsf{s}(c)\circ{\mathsf{inr% }},\mathsf{ap}_{\mathsf{s}(c)}\circ\mathsf{glue})$
		$\displaystyle=({\lambda}a.\,\mathsf{s}(c)({\mathsf{inl}}(a)),\;{\lambda}b.\,% \mathsf{s}(c)({\mathsf{inr}}(b)),\;{\lambda}x.\,\mathsf{ap}_{\mathsf{s}(c)}(% \mathsf{glue}(x)))$
		$\displaystyle=({\lambda}a.\,i(a),\;{\lambda}b.\,j(b),\;{\lambda}x.\,h(x))$
		$\displaystyle\equiv(i,j,h)$
		$\displaystyle=c.$

On the other hand, if $t:A\sqcup^{B}C\to{}E$ , we want to prove that $\mathsf{s}(t\circ c_{\sqcup})=t$ . For $a : A$ , we have

\mathsf{s}(t\circ c_{\sqcup})({\mathsf{inl}}(a))=t({\mathsf{inl}}(a))

because the first component of $t\circ c_{\sqcup}$ is $t\circ{\mathsf{inl}}$ . In the same way, for $b : B$ we have

\mathsf{s}(t\circ c_{\sqcup})({\mathsf{inr}}(b))=t({\mathsf{inr}}(b))

and for $x : C$ we have

\mathsf{ap}_{\mathsf{s}(t\circ c_{\sqcup})}(\mathsf{glue}(x))=\mathsf{ap}_{t}(% \mathsf{glue}(x))

hence $\mathsf{s}(t\circ c_{\sqcup})=t$ .

This proves that $c\mapsto\mathsf{s}(c)$ is a quasi-inverse to $t\mapsto{}t\circ c_{\sqcup}$ , as desired. ∎

A number of standard homotopy-theoretic constructions can be expressed as (homotopy) pushouts.

•

The pushout of the span $\mathbf{1}\leftarrow A\to\mathbf{1}$ is the suspension $\Sigma A$ (see §6.5 (http://planetmath.org/65suspensions)).
•

The pushout of $A\xleftarrow{\mathsf{pr}_{1}}A\times B\xrightarrow{\mathsf{pr}_{2}}B$ is called the join of $A$ and $B$ , written $A*B$ .
•

The pushout of $\mathbf{1}\leftarrow A\xrightarrow{f}B$ is the cone or cofiber of $f$ .
•

If $A$ and $B$ are equipped with basepoints $a_{0}:A$ and $b_{0}:B$ , then the pushout of $A\xleftarrow{a_{0}}\mathbf{1}\xrightarrow{b_{0}}B$ is the wedge $A\vee B$ .
•

If $A$ and $B$ are pointed as before, define $f:A\vee B\to A\times B$ by $f({\mathsf{inl}}(a)):\!\!\equiv(a,b_{0})$ and $f({\mathsf{inr}}(b)):\!\!\equiv(a_{0},b)$ , with ${f}\mathopen{}\left({\mathsf{glue}}\right)\mathclose{}:=\mathsf{refl}_{(a_{0},% b_{0})}$ . Then the cone of $f$ is called the smash product $A\wedge B$ .

We will discuss pushouts further in http://planetmath.org/node/87580Chapter 7,http://planetmath.org/node/87582Chapter 8.

Remark 6.8.3.

As remarked in §3.7 (http://planetmath.org/37propositionaltruncation), the notations $\wedge$ and $\vee$ for the smash product and wedge of pointed spaces are also used in logic for “and” and “or”, respectively. Since types in homotopy type theory can behave either like spaces or like propositions, there is technically a potential for conflict — but since they rarely do both at once, context generally disambiguates. Furthermore, the smash product and wedge only apply to pointed spaces, while the only pointed mere proposition is $\top\equiv\mathbf{1}$ — and we have $\mathbf{1}\wedge\mathbf{1}=\mathbf{1}$ and $\mathbf{1}\vee\mathbf{1}=\mathbf{1}$ for either meaning of $\wedge$ and $\vee$ .

Remark 6.8.4.

Note that colimits do not in general preserve truncatedness. For instance, $\mathbb{S}^{0}$ and $\mathbf{1}$ are both sets, but the pushout of $\mathbf{1}\leftarrow\mathbb{S}^{0}\to\mathbf{1}$ is $\mathbb{S}^{1}$ , which is not a set. If we are interested in colimits in the category of $n$ -types, therefore (and, in particular, in the category of sets), we need to “truncate” the colimit somehow. We will return to this point in §6.9 (http://planetmath.org/69truncations),http://planetmath.org/node/87580Chapter 7,http://planetmath.org/node/87584Chapter 10.

Title	6.8 Pushouts
\metatable