Pushout (HIT)

Definition

The pushout $A{\bigsqcup }_{C}B$ is a Higher Inductive Type that serves as the general colimit form in homotopy type theory.

Given types $A$, $B$, $C$ and functions $f:C\to A$ and $g:C\to B$, the pushout $A{\bigsqcup }_{C}B$ has the following constructors:

• $\mathrm{inl}:A\to A{\bigsqcup }_{C}B$
• $\mathrm{inr}:B\to A{\bigsqcup }_{C}B$
• $\mathrm{glue}:\Pi (c:C).(\mathrm{inl}(f(c))=\mathrm{inr}(g(c)))$

The pushout glues together copies of $A$ and $B$ by identifying $f(c)$ in $A$ with $g(c)$ in $B$ for each $c:C$.

Properties

The pushout is a special case of a Colimit and satisfies the universal property of pushouts from Category Theory.

Related Concepts

Higher Inductive Type Pushout (Category Theory) Suspension (HIT) Colimit Coproduct Type