fact: Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : GroupHomomorphism A B) : {h : B $-> C & h o f == h o g} <~> (GroupCoeq f g $-> C).
imports: Basics Types WildCat.Core Truncations.Core Algebra.Groups.Group Colimits.Coeq Algebra.Groups.FreeProduct