fact: Definition pglue {A B C : Type} {f : A -> B} {g : A -> C} (a : A) : pushl (f a) = pushr (g a) := @cglue A (B+C) (inl o f) (inr o g) a.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq