(a : A) : ap equiv_pushout (pglue a) = ap pushl (p a) @ pglue (eA a) @ ap pushr (q a)^. 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.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.