{B A f g B' A' f' g'} (h : B -> B') (k : A -> A') (p : k o f == f' o h) (q : k o g == g' o h) : @Coeq B A f g -> @Coeq B' A' f' g'. Proof. refine (Coeq_rec _ (coeq o k) _); intros b. refine (ap coeq (p b) @ _ @ ap coeq (q b)^). apply cglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.