proposition: Theorem grp_pres_rec {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: 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. hnf. rapply Trunc_ind. srapply Coeq.Coeq_ind. 2: intros; apply path_ishprop. intros w; hnf. induction w. 1: reflexivity. simpl. refine (_ @ _ @ _^). 1,3: exact (grp_homo_op (FreeGroup_rec _ _ _) _ _). f_ap. destruct a. 1: refine (p _ @ (grp_homo_unit _)^). refine (grp_homo_inv _ _ @ ap _ _ @ (grp_homo_inv _ _)^). refine (p _ @ (grp_homo_unit _)^). } intros p r. hnf in p. pose (p' := p o freegroup_eta). clearbody p'; clear p. specialize (p' (FreeGroup.word_sing _ (inl r))). refine (_ @ p'). clear p'. symmetry. refine (grp_homo_op _ _ _ @ _). refine (_ @ right_identity _). f_ap. Defined.
imports: Basics Types Truncations.Core Algebra.Groups.Group Algebra.Groups.FreeGroup Algebra.Groups.GroupCoeq Spaces.Finite WildCat