{B A} (f g : B -> A) : Coeq f g -> Coeq g f := Coeq_rec (Coeq g f) coeq (fun b : B => (cglue b)^).
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.