fact: Definition Pushout_rec_beta_pglue {A B C f g} (P : Type) (pushb : B -> P) (pushc : C -> P) (pusha : forall a : A, pushb (f a) = pushc (g a)) (a : A) : ap (Pushout_rec P pushb pushc pusha) (pglue a) = pusha a.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq