diff --git a/theories/Algebra/AbGroups/Biproduct.v b/theories/Algebra/AbGroups/Biproduct.v
index 4b4c3b047d5..9d99c6baea0 100644
--- a/theories/Algebra/AbGroups/Biproduct.v
+++ b/theories/Algebra/AbGroups/Biproduct.v
@@ -23,6 +23,46 @@ Definition ab_biprod_inr {A B : AbGroup} : B $-> ab_biprod A B := grp_prod_inr.
 Definition ab_biprod_pr1 {A B : AbGroup} : ab_biprod A B $-> A := grp_prod_pr1.
 Definition ab_biprod_pr2 {A B : AbGroup} : ab_biprod A B $-> B := grp_prod_pr2.
 
+Definition ab_biprod_ind {A B : AbGroup}
+  (P : ab_biprod A B -> Type)
+  (Hinl : forall a, P (ab_biprod_inl a))
+  (Hinr : forall b, P (ab_biprod_inr b))
+  (Hop : forall x y, P x -> P y -> P (x + y))
+  : forall x, P x.
+Proof.
+  intros [a b].
+  snrapply ((grp_prod_decompose a b)^ # _).
+  apply Hop.
+  - exact (Hinl a).
+  - exact (Hinr b).
+Defined.
+
+Definition ab_biprod_ind_homotopy {A B C : AbGroup}
+  {f g : ab_biprod A B $-> C}
+  (Hinl : f $o ab_biprod_inl $== g $o ab_biprod_inl)
+  (Hinr : f $o ab_biprod_inr $== g $o ab_biprod_inr)
+  : f $== g.
+Proof.
+  rapply ab_biprod_ind.
+  - exact Hinl.
+  - exact Hinr.
+  - intros x y p q.
+    lhs nrapply grp_homo_op.
+    rhs nrapply grp_homo_op.
+    f_ap.
+Defined.
+
+(* Maps out of biproducts are determined on the two inclusions. *)
+Definition equiv_ab_biprod_ind_homotopy `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X)
+  : (phi $o ab_biprod_inl == psi $o ab_biprod_inl)
+    * (phi $o ab_biprod_inr == psi $o ab_biprod_inr)
+  <~> phi == psi.
+Proof.
+  apply equiv_iff_hprop.
+  - exact (uncurry ab_biprod_ind_homotopy).
+  - exact (fun h => (fun a => h _, fun b => h _)).
+Defined.
+
 (** Recursion principle *)
 Proposition ab_biprod_rec {A B Y : AbGroup}
             (f : A $-> Y) (g : B $-> Y)
@@ -58,7 +98,7 @@ Proof.
   - exact (left_identity b).
 Defined.
 
-Proposition ab_biprod_rec_inl_beta {A B Y : AbGroup}
+Proposition ab_biprod_rec_beta_inl {A B Y : AbGroup}
             (a : A $-> Y) (b : B $-> Y)
   : (ab_biprod_rec a b) $o ab_biprod_inl == a.
 Proof.
@@ -67,7 +107,7 @@ Proof.
   exact (right_identity (a x)).
 Defined.
 
-Proposition ab_biprod_rec_inr_beta {A B Y : AbGroup}
+Proposition ab_biprod_rec_beta_inr {A B Y : AbGroup}
             (a : A $-> Y) (b : B $-> Y)
   : (ab_biprod_rec a b) $o ab_biprod_inr == b.
 Proof.
@@ -88,9 +128,9 @@ Proof.
   - intros [a b].
     apply path_prod.
     + apply equiv_path_grouphomomorphism.
-      apply ab_biprod_rec_inl_beta.
+      apply ab_biprod_rec_beta_inl.
     + apply equiv_path_grouphomomorphism.
-      apply ab_biprod_rec_inr_beta.
+      apply ab_biprod_rec_beta_inr.
 Defined.
 
 (** Corecursion principle, inherited from Groups/Group.v. *)
@@ -114,6 +154,25 @@ Definition ab_biprod_functor_beta {Z X Y A B : AbGroup} (f0 : Z $-> X) (f1 : Z $
                       $== ab_biprod_corec (g0 $o f0) (g1 $o f1)
   := fun _ => idpath.
 
+Global Instance is0bifunctor_ab_biprod : Is0Bifunctor ab_biprod.
+Proof.
+  srapply Build_Is0Bifunctor'.
+  snrapply Build_Is0Functor.
+  intros [A B] [A' B'] [f g].
+  exact (functor_ab_biprod f g).
+Defined.
+
+Global Instance is1bifunctor_ab_biprod : Is1Bifunctor ab_biprod.
+Proof.
+  snrapply Build_Is1Bifunctor'.
+  snrapply Build_Is1Functor.
+  - intros [A B] [A' B'] [f g] [f' g'] [p q] [a b].
+    snrapply equiv_path_prod.
+    exact (p a, q b).
+  - reflexivity.
+  - cbn; reflexivity.
+Defined.
+
 Definition isequiv_functor_ab_biprod {A A' B B' : AbGroup}
            (f : A $-> A') (g : B $-> B') `{IsEquiv _ _ f} `{IsEquiv _ _ g}
   : IsEquiv (functor_ab_biprod f g).
@@ -175,37 +234,6 @@ Defined.
 
 (** *** Lemmas for working with biproducts *)
 
-Lemma ab_biprod_decompose {B A : AbGroup} (a : A) (b : B)
-  : (a, b) = ((a, group_unit) : ab_biprod A B) + (group_unit, b).
-Proof.
-  apply path_prod; cbn.
-  - exact (right_identity _)^.
-  - exact (left_identity _)^.
-Defined.
-
-Lemma ab_biprod_corec_eta' {A B X : AbGroup} (f g : ab_biprod A B $-> X)
-  : (f $o ab_biprod_inl $== g $o ab_biprod_inl)
-  -> (f $o ab_biprod_inr $== g $o ab_biprod_inr)
-  -> f $== g.
-Proof.
-  intros h k.
-  intros [a b].
-  refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^).
-  exact (grp_homo_op_agree f g (h a) (k b)).
-Defined.
-
-(* Maps out of biproducts are determined on the two inclusions. *)
-Lemma equiv_path_biprod_corec `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X)
-  : ((phi $o ab_biprod_inl == psi $o ab_biprod_inl) * (phi $o ab_biprod_inr == psi $o ab_biprod_inr))
-      <~> phi == psi.
-Proof.
-  apply equiv_iff_hprop.
-  - intros [h k].
-    apply ab_biprod_corec_eta'; assumption.
-  - intro h.
-    exact (fun a => h _, fun b => h _).
-Defined.
-
 (** The swap isomorphism of the biproduct of two groups. *)
 Definition direct_sum_swap {A B : AbGroup}
   : ab_biprod A B $<~> ab_biprod B A.
diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v
index f68984a08f0..bb3c26d6a52 100644
--- a/theories/Algebra/AbGroups/TensorProduct.v
+++ b/theories/Algebra/AbGroups/TensorProduct.v
@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics.
-Require Import Types.Forall Types.Sigma.
+Require Import Types.Forall Types.Sigma Types.Prod.
 Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor.
 Require Import WildCat.NatTrans.
 Require Import Algebra.Groups.Group Algebra.Groups.QuotientGroup.
@@ -807,4 +807,52 @@ Proof.
     reflexivity.
 Defined.
 
+(** ** Tensor products distribute over direct sums *)
+
+Definition ab_tensor_prod_dist_l {A B C : AbGroup}
+  : ab_tensor_prod A (ab_biprod B C)
+    $<~> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C).
+Proof.
+  srapply (let f := _ in let g := _ in cate_adjointify f g _ _).
+  - snrapply ab_tensor_prod_rec.
+    + intros a bc.
+      exact (tensor a (fst bc), tensor a (snd bc)).
+    + intros a bc bc'; cbn beta.
+      snrapply path_prod'; snrapply tensor_dist_l.
+    + intros a a' bc; cbn beta.
+      snrapply path_prod; snrapply tensor_dist_r.
+  - snrapply ab_biprod_rec.
+    + exact (fmap01 ab_tensor_prod A ab_biprod_inl).
+    + exact (fmap01 ab_tensor_prod A ab_biprod_inr).
+  - snrapply ab_biprod_ind_homotopy.
+    + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). 
+      1: snrapply ab_biprod_rec_beta_inl.
+      snrapply ab_tensor_prod_ind_homotopy.
+      intros a b.
+      snrapply path_prod; simpl.
+      * reflexivity.
+      * snrapply tensor_zero_r.
+    + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
+      1: snrapply ab_biprod_rec_beta_inr.
+      snrapply ab_tensor_prod_ind_homotopy.
+      intros a b.
+      snrapply path_prod; simpl.
+      * snrapply tensor_zero_r.
+      * reflexivity.
+  - snrapply ab_tensor_prod_ind_homotopy.
+    intros a [b c].
+    lhs_V nrapply tensor_dist_l; simpl.
+    snrapply ap.
+    symmetry; apply grp_prod_decompose.
+Defined.
+
+Definition ab_tensor_prod_dist_r {A B C : AbGroup}
+  : ab_tensor_prod (ab_biprod A B) C
+    $<~> ab_biprod (ab_tensor_prod A C) (ab_tensor_prod B C).
+Proof.
+  refine (emap11 ab_biprod (braide _ _) (braide _ _)
+    $oE _ $oE braide _ _).
+  snrapply ab_tensor_prod_dist_l.
+Defined.
+
 (** TODO: Show that the category of abelian groups is symmetric closed and therefore we have adjoint pair with the tensor and internal hom. This should allow us to prove lemmas such as tensors distributing over coproducts. *)
diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
index 19e52086f48..5302a52c574 100644
--- a/theories/Algebra/AbSES/Core.v
+++ b/theories/Algebra/AbSES/Core.v
@@ -471,11 +471,11 @@ Proof.
     apply path_sigma_hprop; cbn.
     rapply equiv_path_grouphomomorphism; intros [a b]; cbn.
     apply path_prod; cbn.
-    + rewrite (ab_biprod_decompose a b).
+    + rewrite (grp_prod_decompose a b).
       refine (_ @ (grp_homo_op (ab_biprod_pr1 $o phi) _ _)^).
       apply grp_cancelR; symmetry.
       exact (ap fst (p a)).
-    + rewrite (ab_biprod_decompose a b).
+    + rewrite (grp_prod_decompose a b).
       refine (_ @ (grp_homo_op (ab_biprod_pr2 $o phi) _ _)^); cbn; symmetry.
       exact (ap011 _ (ap snd (p a)) (q (group_unit, b))^).
 Defined.
diff --git a/theories/Algebra/AbSES/PullbackFiberSequence.v b/theories/Algebra/AbSES/PullbackFiberSequence.v
index b7cd4c2e97b..a8a4dce0af9 100644
--- a/theories/Algebra/AbSES/PullbackFiberSequence.v
+++ b/theories/Algebra/AbSES/PullbackFiberSequence.v
@@ -266,7 +266,7 @@ Proof.
   refine (cat_assoc _ _ _ $@ _).
   apply gpd_moveR_Vh.
   apply gpd_moveL_hM.
-  apply equiv_path_biprod_corec.
+  apply equiv_ab_biprod_ind_homotopy.
   split; apply equiv_path_pullback_rec_hset; split; cbn.
   - intro a.
     exact (ap (class_of _ o pullback_pr1) (fst p^$.2 a)).
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 497ebf9885e..c3af650126a 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -907,6 +907,15 @@ Proof.
   intros ? ?; reflexivity.
 Defined.
 
+(** Pairs in direct products can be decomposed *)
+Definition grp_prod_decompose {G H : Group} (g : G) (h : H)
+  : (g, h) = ((g, group_unit) : grp_prod G H) * (group_unit, h).
+Proof.
+  snrapply path_prod; symmetry.
+  - snrapply grp_unit_r.
+  - snrapply grp_unit_l.
+Defined.
+
 (** The second projection is a surjection. *)
 Global Instance issurj_grp_prod_pr2 {G H : Group}
   : IsSurjection (@grp_prod_pr2 G H)