(b : B) (a' : A') : ap (fun x => Coeq_rec2 x (coeq a')) (cglue b) = cgluel b a'. Proof. nrapply Coeq_rec_beta_cglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.