@Coeq B' A' f' g' -> @Coeq B A f g. Proof. refine (functor_coeq h^-1 k^-1 _ _). - intros b. refine (ap (k^-1 o f') (eisretr h b)^ @ _ @ eissect k (f (h^-1 b))). apply ap, inverse, p. - intros b. refine (ap (k^-1 o g') (eisretr h b)^ @ _ @ eissect k (g (h^-1 b))). apply ap, inverse, q. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.