Pushout (Category Theory)

In category theory, pushouts are the dual notion of pullbacks. Formally, pushouts are a colimit of a diagram of this form:

$$\text{require}AMScd\begin{array}{ccc}A& \stackrel{f}{\to }& B\\ g\downarrow & & \\ C& & \end{array}$$

As a HIT

As a higher inductive type, a pushout can be written as $A{\bigsqcup }_{C}B$ for types $A,B,C$ and functions $f:C\to A$ and $g:C\to B$. Defined inductively from the following constructors:

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