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 colimitsMathworldPlanetmath. 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 productMathworldPlanetmath types have the correct universal propertyMathworldPlanetmath of a categorical product of types, and in http://planetmath.org/node/87640Exercise 2.9 that coproductMathworldPlanetmath 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 pullbackPlanetmathPlanetmath of f:AC and g:BC is (a:A)(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 sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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 ACB presented by

  • a function 𝗂𝗇𝗅:AACB,

  • a function 𝗂𝗇𝗋:BACB, and

  • for each c:C a path 𝗀𝗅𝗎𝖾(c):(𝗂𝗇𝗅(f(c))=𝗂𝗇𝗋(g(c))).

In other words, ACB is the disjoint unionMathworldPlanetmathPlanetmath 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:ACBD by defining

  • for each a:A, the value of s(𝗂𝗇𝗅(a)):D,

  • for each b:B, the value of s(𝗂𝗇𝗋(b)):D, and

  • for each c:C, the value of 𝖺𝗉s(𝗀𝗅𝗎𝖾(c)):s(𝗂𝗇𝗅(f(c)))=s(𝗂𝗇𝗋(g(c))).

We leave it to the reader to formulate the inductionMathworldPlanetmath principle. It also implies the uniqueness principle that if s,s:ACBD are two maps such that

s(𝗂𝗇𝗅(a)) =s(𝗂𝗇𝗅(a))
s(𝗂𝗇𝗋(b)) =s(𝗂𝗇𝗋(b))
𝖺𝗉s(𝗀𝗅𝗎𝖾(c)) =𝖺𝗉s(𝗀𝗅𝗎𝖾(c))  (modulo the previous two equalities)

for every a,b,c, then s=s.

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

Definition 6.8.1.

Given a span D=(A𝑓C𝑔B) and a type D, a cocone under D with vertex D consists of functions i:AD and j:BD and a homotopy h:(c:C)(i(f(c))=j(g(c))):



We denote by coconeD(D) the type of all such cocones, i.e.


Of course, there is a canonical cocone under 𝒟 with vertex ACB consisting of 𝗂𝗇𝗅, 𝗂𝗇𝗋, and 𝗀𝗅𝗎𝖾.



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

Lemma 6.8.2.

For any type E, there is an equivalence


Let’s consider an arbitrary type E:𝒰. There is a canonical function


defined by sending (i,j,h) to (ti,tj,𝖺𝗉th). We show that this is an equivalence.

Firstly, given a c=(i,j,h):𝖼𝗈𝖼𝗈𝗇𝖾𝒟(E), we need to construct a map 𝗌(c) from ACB to E.



The map 𝗌(c) is defined in the following way

𝗌(c)(𝗂𝗇𝗅(a)) :i(a),
𝗌(c)(𝗂𝗇𝗋(b)) :j(b),
𝖺𝗉𝗌(c)(𝗀𝗅𝗎𝖾(x)) :=h(x).

We have defined a map


and we need to prove that this map is an inversePlanetmathPlanetmathPlanetmath to ttc. On the one hand, if c=(i,j,h):𝖼𝗈𝖼𝗈𝗇𝖾𝒟(E), we have

𝗌(c)c =(𝗌(c)𝗂𝗇𝗅,𝗌(c)𝗂𝗇𝗋,𝖺𝗉𝗌(c)𝗀𝗅𝗎𝖾)

On the other hand, if t:ABCE, we want to prove that 𝗌(tc)=t. For a:A, we have


because the first component of tc is t𝗂𝗇𝗅. In the same way, for b:B we have


and for x:C we have


hence 𝗌(tc)=t.

This proves that c𝗌(c) is a quasi-inversePlanetmathPlanetmath to ttc, as desired. ∎

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

  • The pushout of the span 𝟏A𝟏 is the suspension ΣA (see §6.5 (http://planetmath.org/65suspensions)).

  • The pushout of A𝗉𝗋1A×B𝗉𝗋2B is called the join of A and B, written A*B.

  • The pushout of 𝟏A𝑓B is the cone or cofiber of f.

  • If A and B are equipped with basepoints a0:A and b0:B, then the pushout of Aa0𝟏b0B is the wedge AB.

  • If A and B are pointed as before, define f:ABA×B by f(𝗂𝗇𝗅(a)):(a,b0) and f(𝗂𝗇𝗋(b)):(a0,b), with f(𝗀𝗅𝗎𝖾):=𝗋𝖾𝖿𝗅(a0,b0). Then the cone of f is called the smash product AB.

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 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 propositionsPlanetmathPlanetmath, 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 1 — and we have 11=1 and 11=1 for either meaning of and .

Remark 6.8.4.

Note that colimits do not in general preserve truncatedness. For instance, S0 and 1 are both sets, but the pushout of 1S01 is S1, which is not a set. If we are interested in colimits in the categoryMathworldPlanetmath 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