{A B : AbGroup} (P : ab_tensor_prod A B -> Type) {H : forall x, IsHProp (P x)} (Hin : forall a b, P (tensor a b)) (Hop : forall x y, P x -> P y -> P (x + y)) : forall x, P x. Proof. unfold ab_tensor_prod. srapply grp_quotient_ind_hprop. srapply Abel_ind_hprop; cbn beta. set (tensor_in := grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B). change (forall x, P (tensor_in x)). srapply FreeGroup_ind_hprop'; intros w; cbn beta. induction w. - exact (transport P (tensor_zero_l 0) (Hin 0 0)). - change (P (tensor_in (freegroup_eta [a]%list + freegroup_eta w))). rewrite grp_homo_op. destruct a as [[a b]|[a b]]. + change (P (tensor_in (freegroup_in (a, b)) + tensor_in (freegroup_eta w))). apply Hop; trivial. apply Hin. + change (P (tensor_in (- freegroup_in (a, b)) + tensor_in (freegroup_eta w))). rewrite grp_homo_inv. apply Hop; trivial. rewrite <- tensor_neg_l. apply Hin. 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.