{A} : ab_tensor_prod A abgroup_Z $<~> A. Proof. symmetry. snrapply Build_GroupIsomorphism. - nrapply grp_homo_tensor_r. exact 1%int. - snrapply isequiv_adjointify. + snrapply ab_tensor_prod_rec'. * exact grp_pow_homo. * intros a a' z; cbn beta. nrapply (grp_homo_op (ab_mul z)). + hnf. change (forall x : ?A, (grp_homo_map ?f) ((grp_homo_map ?g) x) = x) with (f $o g $== Id _). snrapply ab_tensor_prod_ind_homotopy. intros a z. change (tensor (B:=abgroup_Z) (grp_pow a z) 1%int = tensor a z). lhs nrapply tensor_ab_mul. nrapply ap. lhs nrapply abgroup_Z_ab_mul. apply int_mul_1_r. + exact grp_unit_r. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Sigma Types.Prod. Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor. Require Import WildCat.NatTrans WildCat.MonoidalTwistConstruction. Require Import Algebra.Groups.Group Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Algebra.AbGroups.AbHom Algebra.AbGroups.FreeAbelianGroup. Require Import Algebra.AbGroups.Abelianization Algebra Algebra.Groups.FreeGroup. Require Import Colimits.Quotient. Require Import Spaces.List.Core Spaces.Int. Require Import AbGroups.Z. Require Import Truncations.