nLab pushout type

Idea

In homotopy type theory, a homotopy pushout type is a kind of higher inductive type whose categorical semantics is that of homotopy pushouts.

Definition

As a higher inductive type

The (homotopy) pushout of a span $A \xleftarrow{f} C \xrightarrow{g} B$ is the higher inductive type $A \sqcup^{C}_{f ; g} B$ (or $A \sqcup^C B$) generated by:

• a function $inl : A \to A \sqcup^{C} B$
• a function $inr : B \to A \sqcup^{C} B$
• for each $c:C$ a path $glue(c) : inl (f (c)) = inr (g( c))$

In Coq pseudocode:

Inductive hpushout {A B C : Type} (f : A -> B) (g : A -> C) : Type :=
| inl : B -> hpushout f g
| inr : C -> hpushout f g
| glue : forall (a : A), inl (f a) == inr (g a).

Inference rules

Explicitly, this means that the inference rules for pushout types are as follows (where we now label terms as shown in the following diagram):

type formation rule:

$$\frac{ \begin{array}{l} X,\, Y,\, Y^' \,\colon\, Type \;; \;\; f \,\colon\, X \to Y \;, \;\; f^' \,\colon\, X \to Y^' \mathclap{\phantom{\vert_{\vert}}} \end{array} } { \mathclap{\phantom{\vert^{\vert}}} Y \underset{X}{\sqcup} Y^' \,\colon\, Type }$$

term introduction rules:

$$\frac{ y \,\colon\, Y \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} cpr(y) \,\colon\, Y \underset{X}{\sqcup} Y^' } \;\;\;\;\;\;\;\;\; \frac{ y^' \,\colon\, Y^' \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} cpr^'(y^') \,\colon\, Y \underset{X}{\sqcup} Y^' } \;\;\;\;\;\;\;\;\; \frac{ x \,\colon\, X \mathclap{\phantom{\vert}} }{ \mathclap{\phantom{\vert^{\vert^{\vert}}}} hmt(x) \,\colon\, Id_{\big(Y \underset{X}{\sqcup} Y^'\big)} \Big( cpr\big(f(x)\big) ,\, cpr^'\big(f^'(x)\big) \Big) }$$

term elimination rule:

$$\frac{ \begin{array}{l} \hat{y} \,\colon\, Y \underset{X}{\sqcup} Y^' \;\vdash\; P(\hat{y}) \,\colon\, Type \;; \\ cpr_P \,\colon\, \underset{ y \colon Y }{\prod} P\big( cpr(y) \big) \;; \;\; cpr^'_P \,\colon\, \underset{ y^' \colon Y^' }{\prod} P\big( cpr^'(y^') \big) \;; \\ hmt_P \,\colon\, \underset{x \colon X}{\prod} Id_{P\Big( cpr^'\big(f^'(x)\big) \Big)} \bigg( hmt(x)_\ast \Big( cpr_P\big( f(x) \big) \Big) ,\, cpr^'_P\big( f^'(x) \big) \bigg) \end{array} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)} \,\colon\, \underset{ \hat{y} \,\colon\, Y \underset{X}{\sqcup} Y^' }{\prod} \, P(\hat{y}) }$$

computation rules:

$$\frac{ \begin{array}{l} \hat{y} \,\colon\, Y \underset{X}{\sqcup} Y^' \;\vdash\; P(\hat{y}) \,\colon\, Type \;; \\ cpr_P \,\colon\, \underset{ y \colon Y }{\prod} P\big( cpr^'(y) \big) \;; \;\; cpr^'_P \,\colon\, \underset{ y^' \colon Y^' }{\prod} P\big( cpr^'(y^') \big) \;; \\ hmt_P \,\colon\, \underset{x \colon X}{\prod} Id_{P(x)} \bigg( hmt(x)_\ast \Big( cpr_P\big( f(x) \big) \Big) ,\, cpr^'_P\big( cpr^'(x) \big) \bigg) \end{array} }{ \begin{array}{rlc} \mathclap{\phantom{\vert^{\vert}}} ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)} \,\circ\, cpr &=& cpr_P \;; \\ \mathclap{\phantom{\vert^{\vert}}} ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)} \,\circ\, cpr^' &=& cpr^'_P \;; \\ happly_{\big( ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)} \big)} \,\circ\, hmt &=& hmt_P \end{array} }$$

Here:

• “$Id_X$” denotes the identity type of the type $X$;

• “=” denotes judgemental equality;

• “$happly$” denotes the dependently typed version of the operation here.

Examples

• suspension type

• join type

• wedge sum type

• smash product type

• cofiber type

See also

• higher inductive type

• dependent pushout type

• pushout, homotopy pushout

References

Early discussion of the idea of homotopy pushouts as higher inductive types:

• Mike Shulman, Homotopy Type Theory VI (2011) [blog post]

Many references on higher inductive types mention pushout types and highlight their categorical semantics, but skip type-theoretic details, e.g.:

• Univalent Foundations Project, §6.8 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

The full inference rules are stated in:

• Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, p. 4 of: A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, LICS ‘16 (2016) 565–574 [arXiv.1605.03227, doi:10.1145/2933575.2934545]

as well as in section 6 of:

• Peter LeFanu Lumsdaine, Mike Shulman, Semantics of higher inductive types, Math. Proc. Camb. Phil. Soc. 169 (2020) 159-208 [arXiv:1705.07088, talk slides pdf, doi:10.1017/S030500411900015X]

See also:

• Egbert Rijke, Homotopy pushouts [pdf], Lecture 13 in: Introduction to Homotopy Type Theory, lecture notes, CMU (2018) [pdf, pdf, webpage]

Formalization in the Coq proof assistant:

• Guillaume Brunerie, HoTT/Coq/Limits/Pullbacks.v