proposition: Lemma equiv_Z1_hom@{u v | u < v} `{Funext} (A : AbGroup@{u}) : GroupIsomorphism (ab_hom@{u v} ab_Z1@{u v} A) A.
proof: Proof. snrapply Build_GroupIsomorphism'. - refine (_ oE (equiv_freegroup_rec@{u u u v} A Unit)^-1). symmetry. refine (Build_Equiv _ _ (fun a => unit_name a) _). - intros f g. cbn. reflexivity. Defined.
imports: Basics Types WildCat.Core Truncations.Core AbelianGroup AbHom Centralizer AbProjective Groups.FreeGroup AbGroups.Z Int.Core