Contents

# Contents

## 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.

## References

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

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

The full inference rules are stated in: