Pushout@{i j k l} {A : Type@{i}} {B : Type@{j}} {C : Type@{k}} (f : A -> B) (g : A -> C) : Type@{l} := Coeq@{l l _} (inl o f) (inr o g).
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.