{funext : Funext} (G : Group) (P : HasPresentation G) (H : Group) : {f : gp_generators P -> H & forall r, FreeGroup_rec _ _ f (gp_relators P r) = group_unit} <~> GroupHomomorphism G H. Proof. refine ((equiv_precompose_cat_equiv grp_iso_presentation)^-1 oE _). refine (equiv_groupcoeq_rec _ _ oE _). srefine (equiv_functor_sigma_pb _ oE _). 2: apply equiv_freegroup_rec. apply equiv_functor_sigma_id. intros f. srapply equiv_iff_hprop. { intros p. change (equiv_freegroup_rec H _ f $o FreeGroup_rec _ _ (gp_relators P) $== equiv_freegroup_rec _ _ f $o FreeGroup_rec _ _ (fun _ => group_unit)). rapply FreeGroup_ind_homotopy. exact p. } intros p r. hnf in p. exact (p (freegroup_in r)). Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.FreeGroup. Require Import Algebra.Groups.GroupCoeq. Require Import Spaces.Finite Spaces.List.Core. Require Import WildCat.