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 -types, e.g. the pullback of and is (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:
The pushout of this span is the higher inductive type presented by
a function ,
a function , and
for each a path .
for each , the value of ,
for each , the value of , and
for each , the value of .
We leave it to the reader to formulate the induction principle. It also implies the uniqueness principle that if are two maps such that
for every , then .
To formulate the universal property of a pushout, we introduce the following.
Given a span and a type , a cocone under with vertex consists of functions and and a homotopy :
We denote by the type of all such cocones, i.e.
Of course, there is a canonical cocone under with vertex consisting of , , and .
The following lemma says that this is the universal such cocone.
For any type , there is an equivalence
Let’s consider an arbitrary type . There is a canonical function
defined by sending to . We show that this is an equivalence.
Firstly, given a , we need to construct a map from to .
The map is defined in the following way
We have defined a map
and we need to prove that this map is an inverse to . On the one hand, if , we have
On the other hand, if , we want to prove that . For , we have
because the first component of is . In the same way, for we have
and for we have
This proves that is a quasi-inverse to , as desired. ∎
A number of standard homotopy-theoretic constructions can be expressed as (homotopy) pushouts.
The pushout of the span is the suspension (see §6.5 (http://planetmath.org/65suspensions)).
The pushout of is called the join of and , written .
The pushout of is the cone or cofiber of .
If and are equipped with basepoints and , then the pushout of is the wedge .
If and are pointed as before, define by and , with . Then the cone of is called the smash product .
We will discuss pushouts further in http://planetmath.org/node/87580Chapter 7,http://planetmath.org/node/87582Chapter 8.
As remarked in §3.7 (http://planetmath.org/37propositionaltruncation), the notations and 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 — and we have and for either meaning of and .
Note that colimits do not in general preserve truncatedness. For instance, and are both sets, but the pushout of is , which is not a set. If we are interested in colimits in the category of -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.