A {B C} (f g : B $-> C) : ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g) $<~> ab_tensor_prod A (ab_coeq f g). Proof. snrapply cate_adjointify. - snrapply ab_coeq_rec. + rapply (fmap01 ab_tensor_prod A). nrapply ab_coeq_in. + refine (_^$ $@ fmap02 ab_tensor_prod _ _ $@ _). 1,3: rapply fmap01_comp. nrapply ab_coeq_glue. - snrapply ab_tensor_prod_rec'. + intros a. snrapply functor_ab_coeq. 1,2: snrapply (grp_homo_tensor_l a). 1,2: hnf; reflexivity. + intros a a'; cbn beta. srapply ab_coeq_ind_hprop. intros x. exact (ap (ab_coeq_in (f:=fmap01 ab_tensor_prod A f) (g:=fmap01 ab_tensor_prod A g)) (tensor_dist_r a a' x)). - snrapply ab_tensor_prod_ind_homotopy. intros a. srapply ab_coeq_ind_hprop. intros c. reflexivity. - snrapply ab_coeq_ind_homotopy. snrapply ab_tensor_prod_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.