proposition: Lemma equiv_pushout_pglue (a : A) : ap equiv_pushout (pglue a) = ap pushl (p a) @ pglue (eA a) @ ap pushr (q a)^.
proof: Proof. refine (functor_coeq_beta_cglue _ _ _ _ a @ _). refine (_ @@ 1 @@ _). - symmetry; refine (ap_compose inl coeq _). - refine (ap (ap coeq) (ap_V _ _)^ @ _). symmetry; refine (ap_compose inr coeq _). Defined.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq