X Y : FreeAbGroup (X * Y) $<~> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y). Proof. srefine (let f:=_ in let g:=_ in cate_adjointify f g _ _). - snrapply FreeAbGroup_rec. intros [x y]. exact (tensor (freeabgroup_in x) (freeabgroup_in y)). - snrapply ab_tensor_prod_rec. + intros x. snrapply FreeAbGroup_rec. intros y; revert x. unfold FreeAbGroup. snrapply FreeAbGroup_rec. intros x. apply abel_unit. apply freegroup_in. exact (x, y). + intros x y y'. snrapply grp_homo_op. + intros x x'. rapply Abel_ind_hprop. snrapply (FreeGroup_ind_homotopy _ (f' := ab_homo_add _ _)). intros y. lhs nrapply FreeGroup_rec_beta. lhs nrapply grp_homo_op. snrapply (ap011 (+) _^ _^). 1,2: nrapply FreeGroup_rec_beta. - snrapply ab_tensor_prod_ind_homotopy. intros x. change (f $o g $o grp_homo_tensor_l x $== grp_homo_tensor_l x). rapply Abel_ind_hprop. change (@abel_in ?G) with (grp_homo_map (@abel_unit G)). repeat change (cat_comp (A:=AbGroup) ?f ?g) with (cat_comp (A:=Group) f g). change (forall y, grp_homo_map ?f (abel_unit y) = grp_homo_map ?g (abel_unit y)) with (cat_comp (A:=Group) f abel_unit $== cat_comp (A:=Group) g abel_unit). rapply FreeGroup_ind_homotopy. intros y; revert x. change (f $o g $o grp_homo_tensor_r (freeabgroup_in y) $== grp_homo_tensor_r (freeabgroup_in y)). rapply Abel_ind_hprop. change (@abel_in ?G) with (grp_homo_map (@abel_unit G)). repeat change (cat_comp (A:=AbGroup) ?f ?g) with (cat_comp (A:=Group) f g). change (forall y, grp_homo_map ?f (abel_unit y) = grp_homo_map ?g (abel_unit y)) with (cat_comp (A:=Group) f abel_unit $== cat_comp (A:=Group) g abel_unit). rapply FreeGroup_ind_homotopy. intros x. reflexivity. - rapply Abel_ind_hprop. change (GpdHom (A:=Hom(A:=Group) (FreeGroup (X * Y)) _) (cat_comp (A:=Group) (g $o f) (@abel_unit (FreeGroup (X * Y)))) (@abel_unit (FreeGroup (X * Y)))). snrapply FreeGroup_ind_homotopy. reflexivity. 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.