{B A f g} b : @coeq B A f g (f b) = coeq (g b) := gqglue (b; (idpath,idpath)).
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.