fact: Definition cglue {B A f g} b : @coeq B A f g (f b) = coeq (g b) := gqglue (b; (idpath,idpath)).
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod Cubical.DPath Colimits.GraphQuotient