(G : Group) (s : A -> G) : GroupHomomorphism FreeGroup G. Proof. snrapply Build_GroupHomomorphism. { rapply Trunc_rec. srapply Coeq_rec. 1: apply words_rec, s. intros [[b a] c]. apply words_rec_coh. } intros x y; strip_truncations. revert x; srapply Coeq_ind_hprop; intro x. revert y; srapply Coeq_ind_hprop; intro y. simpl. apply words_rec_pp. Defined.
Require Import Basics Types Group Subgroup