\begin{code}
{-# OPTIONS --safe #-}

module Examples.Pushout where
open import Prelude

module _ {A B C : Type} where
\end{code}
%<*pushout>
\begin{code}
  data Pushout (f : A → B) (g : A → C) : Type where
    inl  : B  → Pushout f g
    inr  : C  → Pushout f g
    push  : ∀ i → inl (f i) ≡ inr (g i)
    trunc : isSet (Pushout f g)
\end{code}
%</pushout>