Contents

# Contents

## Idea

The pushout type is an axiomatization of the homotopy pushout in the context of homotopy type theory.

## Definition

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