diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v
index 26793306e21..bcc5624a86b 100644
--- a/theories/Algebra/AbGroups/AbPushout.v
+++ b/theories/Algebra/AbGroups/AbPushout.v
@@ -28,7 +28,7 @@ Proof.
   - intros [x y] q; strip_truncations; simpl.
     destruct q as [a q]. cbn in q.
     refine (ap (uncurry (fun x y => b x + c y)) q^ @ _).
-    unfold uncurry; cbn.
+    cbn.
     refine (ap011 sg_op (preserves_negate _) (p a)^ @ _).
     exact (left_inverse _).
 Defined.
diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 7c9a818bbed..2dbff11b801 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -38,6 +38,12 @@ Global Instance negate_abgroup (A : AbGroup) : Negate A := group_inverse.
 Definition ab_comm {A : AbGroup} (x y : A) : x + y = y + x
   := commutativity x y.
 
+Definition ab_neg_op {A : AbGroup} (x y : A) : - (x + y) = -x - y.
+Proof.
+  lhs nrapply grp_inv_op.
+  apply ab_comm.
+Defined.
+
 (** ** Paths between abelian groups *)
 
 Definition equiv_path_abgroup `{Univalence} {A B : AbGroup@{u}}
@@ -100,6 +106,8 @@ Defined.
 Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup
   := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _).
 
+Arguments QuotientAbGroup G H : simpl never.
+
 Definition quotient_abgroup_rec {G : AbGroup}
   (N : Subgroup G) (H : AbGroup)
   (f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit)
diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index 55fe3b10441..e30e3127cd1 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/theories/Algebra/AbGroups/Abelianization.v
@@ -52,10 +52,10 @@ From this we can show that Abel G is an abelian group.
 In fact this models the following HIT:
 
 HIT Abel (G : Group) := 
- | ab : G -> Abel G
- | ab_comm : forall x y z, ab (x * (y * z)) = ab (x * (z * y)).
+ | abel_in : G -> Abel G
+ | abel_in_comm : forall x y z, abel_in (x * (y * z)) = abel_in (x * (z * y)).
 
-We also derive ab and ab_comm from our coequalizer definition, and even prove the induction and computation rules for this HIT.
+We also derive [abel_in] and [abel_in_comm] from our coequalizer definition, and even prove the induction and computation rules for this HIT.
 
 This HIT was suggested by Dan Christensen.
 *)
@@ -80,15 +80,15 @@ Section Abel.
       (uncurry2 (fun a b c : G => a * (c * b)))).
 
   (** We have a natural map from G to Abel G. *)
-  Definition ab : G -> Abel.
+  Definition abel_in : G -> Abel.
   Proof.
     intro g.
     apply tr, coeq, g.
   Defined.
 
   (** This map satisfies the condition ab_comm. *)
-  Definition ab_comm a b c
-    : ab (a * (b * c)) = ab (a * (c * b)).
+  Definition abel_in_comm a b c
+    : abel_in (a * (b * c)) = abel_in (a * (c * b)).
   Proof.
     apply (ap tr).
     exact (cglue (a, b, c)).
@@ -99,8 +99,8 @@ Section Abel.
 
   (** We can derive the induction principle from the ones for truncation and the coequalizer. *)
   Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)} 
-    (a : forall x, P (ab x)) (c : forall x y z, DPath P (ab_comm x y z)
-      (a (x * (y * z))) (a (x * (z * y))))
+    (a : forall x, P (abel_in x))
+    (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y))))
     : forall (x : Abel), P x.
   Proof.
     srapply Trunc_ind.
@@ -111,19 +111,28 @@ Section Abel.
     apply c.
   Defined.
 
-  (** The computation rule can also be proven. *)
-  Definition Abel_ind_beta_ab_comm (P : Abel -> Type)
-    `{forall x, IsHSet (P x)}(a : forall x, P (ab x))
-    (c : forall x y z, DPath P (ab_comm x y z)
-      (a (x * (y * z))) (a (x * (z * y))))
-    (x y z : G) : apD (Abel_ind P a c) (ab_comm x y z) = c x y z.
+  (** The computation rule on point constructors holds definitionally. *)
+  Definition Abel_ind_beta_abel_in (P : Abel -> Type) `{forall x, IsHSet (P x)}
+    (a : forall x, P (abel_in x))
+    (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y))))
+    (x : G)
+    : Abel_ind P a c (abel_in x) = a x
+    := idpath.
+
+  (** The computation rule on paths. *)
+  Definition Abel_ind_beta_abel_in_comm (P : Abel -> Type) `{forall x, IsHSet (P x)}
+    (a : forall x, P (abel_in x))
+    (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y))))
+    (x y z : G)
+    : apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z.
   Proof.
     refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _).
     rapply Coeq_ind_beta_cglue.
   Defined.
 
   (** We also have a recursion princple. *)
-  Definition Abel_rec (P : Type) `{IsHSet P} (a : G -> P)
+  Definition Abel_rec (P : Type) `{IsHSet P}
+    (a : G -> P)
     (c : forall x y z, a (x * (y * z)) = a (x * (z * y)))
     : Abel -> P.
   Proof.
@@ -131,9 +140,10 @@ Section Abel.
     intros; apply dp_const, c.
   Defined.
 
-  (** Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths. *)
+  (** Here is a simpler version of [Abel_ind] when our target is an [HProp]. This lets us discard all the higher paths. *)
   Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)} 
-    (a : forall x, P (ab x)) : forall (x : Abel), P x.
+    (a : forall x, P (abel_in x))
+    : forall (x : Abel), P x.
   Proof.
     srapply (Abel_ind _ a).
     intros; apply path_ishprop.
@@ -141,7 +151,8 @@ Section Abel.
 
   (** And its recursion version. *)
   Definition Abel_rec_hprop (P : Type) `{IsHProp P}
-    (a : G -> P) : Abel -> P.
+    (a : G -> P)
+    : Abel -> P.
   Proof.
     apply (Abel_rec _ a).
     intros; apply path_ishprop.
@@ -152,9 +163,10 @@ End Abel.
 (** The [IsHProp] argument of [Abel_ind_hprop] can usually be found by typeclass resolution, but [srapply] is slow, so we use this tactic instead. *)
 Local Ltac Abel_ind_hprop x := snrapply Abel_ind_hprop; [exact _ | intro x].
 
-(** We make sure that G is implicit in the arguments of ab and ab_comm. *)
-Arguments ab {_}.
-Arguments ab_comm {_}.
+(** We make sure that G is implicit in the arguments of [abel_in
+ and [abel_in_comm]. *)
+Arguments abel_in {_}.
+Arguments abel_in_comm {_}.
 
 (** Now we can show that Abel G is in fact an abelian group. *)
 
@@ -163,7 +175,9 @@ Section AbelGroup.
   Context (G : Group).
 
   (** Firstly we derive the operation on Abel G. This is defined as follows:
-        ab x + ab y := ab (x y)
+      <<
+        abel_in x + abel_in y := abel_in (x * y)
+      >>
       But we need to also check that it preserves ab_comm in the appropriate way. *)
   Global Instance abel_sgop : SgOp (Abel G).
   Proof.
@@ -173,21 +187,21 @@ Section AbelGroup.
       revert a.
       srapply Abel_rec.
       { intro a.
-        exact (ab (a * b)). }
+        exact (abel_in (a * b)). }
       intros a c d; hnf.
       (* The pattern seems to be to alternate associativity and ab_comm. *)
       refine (ap _ (associativity _ _ _)^ @ _).
-      refine (ab_comm _ _ _ @ _).
+      refine (abel_in_comm _ _ _ @ _).
       refine (ap _ (associativity _ _ _) @ _).
-      refine (ab_comm _ _ _ @ _).
+      refine (abel_in_comm _ _ _ @ _).
       refine (ap _ (associativity _ _ _)^ @ _).
-      refine (ab_comm _ _ _ @ _).
+      refine (abel_in_comm _ _ _ @ _).
       refine (ap _ (associativity _ _ _)). }
     intros b c d.
     revert a.
     Abel_ind_hprop a; simpl.
     refine (ap _ (associativity _ _ _) @ _).
-    refine (ab_comm _ _ _ @ _).
+    refine (abel_in_comm _ _ _ @ _).
     refine (ap _ (associativity _ _ _)^).
   Defined.
 
@@ -205,7 +219,7 @@ Section AbelGroup.
   Global Instance abel_issemigroup : IsSemiGroup (Abel G) := {}.
 
   (** We define the unit as ab of the unit of G *)
-  Global Instance abel_mon_unit : MonUnit (Abel G) := ab mon_unit.
+  Global Instance abel_mon_unit : MonUnit (Abel G) := abel_in mon_unit.
 
   (** By using Abel_ind_hprop we can prove the left and right identity laws. *)
   Global Instance abel_leftidentity : LeftIdentity abel_sgop abel_mon_unit.
@@ -230,25 +244,30 @@ Section AbelGroup.
     Abel_ind_hprop y.
     revert x.
     Abel_ind_hprop x.
-    refine ((ap ab (left_identity _))^ @ _).
-    refine (_ @ (ap ab (left_identity _))).
-    apply ab_comm.
+    refine ((ap abel_in (left_identity _))^ @ _).
+    refine (_ @ (ap abel_in (left_identity _))).
+    apply abel_in_comm.
   Defined.
 
   (** Now we can define the negation. This is just
-        - (ab g) := (ab (g^-1))
+      <<
+        - (abel_in g) := abel_in (- g)
+      >>
       However when checking that it respects ab_comm we have to show the following:
-        ab (- z * - y * - x) = ab (- y * - z * - x)
-      there is no obvious way to do this, but we note that ab (x * y) is exactly the definition of ab x + ab y! Hence by commutativity we can show this. *)
+      <<
+        abel_in (- z * - y * - x) = abel_in (- y * - z * - x)
+      >>
+      there is no obvious way to do this, but we note that [abel_in (x * y)] is exactly the definition of [abel_in x + abel_in y]! Hence by commutativity we can show this. *)
   Global Instance abel_negate : Negate (Abel G).
   Proof.
     srapply Abel_rec.
     { intro g.
-      exact (ab (-g)). }
+      exact (abel_in (-g)). }
     intros x y z; cbn.
     rewrite ?negate_sg_op.
-    change (ab(- z) * ab(- y) * ab (- x) = ab (- y) * ab (- z) * ab(- x)).
-    by rewrite (commutativity (ab (-z)) (ab (-y))).
+    change (abel_in (- z) * abel_in (- y) * abel_in (- x)
+      = abel_in (- y) * abel_in (- z) * abel_in (- x)).
+    by rewrite (commutativity (abel_in (-z)) (abel_in (-y))).
   Defined.
 
   (** Again by Abel_ind_hprop and the corresponding laws for G we can prove the left and right inverse laws. *)
@@ -270,16 +289,16 @@ Section AbelGroup.
   (** And since the operation is commutative, an abelian group. *)
   Global Instance isabgroup_abel : IsAbGroup (Abel G) := {}.
 
-  (** By definition, the map ab is also a group homomorphism. *)
-  Global Instance issemigrouppreserving_ab : IsSemiGroupPreserving ab.
+  (** By definition, the map [abel_in] is also a group homomorphism. *)
+  Global Instance issemigrouppreserving_abel_in : IsSemiGroupPreserving abel_in.
   Proof.
     by unfold IsSemiGroupPreserving.
   Defined.
 
 End AbelGroup.
 
-(** We can easily prove that ab is a surjection. *)
-Global Instance issurj_ab {G : Group} : IsSurjection (@ab G).
+(** We can easily prove that [abel_in] is a surjection. *)
+Global Instance issurj_abel_in {G : Group} : IsSurjection (@abel_in G).
 Proof.
   apply BuildIsSurjection.
   Abel_ind_hprop x.
@@ -300,14 +319,12 @@ Proof.
   - exact _.
 Defined.
 
-(** The unit of this map is the map ab which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *)
-Definition abel_unit (X : Group)
-  : GroupHomomorphism X (abel X).
-Proof.
-  snrapply @Build_GroupHomomorphism.
-  + exact ab.
-  + exact _.
-Defined.
+Arguments abel G : simpl never.
+
+(** The unit of this map is the map [abel_in] which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *)
+Definition abel_unit {G : Group}
+  : GroupHomomorphism G (abel G)
+  := @Build_GroupHomomorphism G (abel G) abel_in _.
 
 Definition grp_homo_abel_rec {G : Group} {A : AbGroup} (f : G $-> A)
   : abel G $-> A.
@@ -315,8 +332,7 @@ Proof.
   snrapply Build_GroupHomomorphism.
   { srapply (Abel_rec _ _ f).
     intros x y z.
-    refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
-    apply (ap (_ *.)).
+    nrapply grp_homo_op_agree; trivial.
     refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
     apply commutativity. }
   intros y.
@@ -327,7 +343,7 @@ Defined.
 
 (** Finally we can prove that our construction abel is an abelianization. *)
 Global Instance isabelianization_abel {G : Group}
-  : IsAbelianization (abel G) (abel_unit G).
+  : IsAbelianization (abel G) abel_unit.
 Proof.
   intros A. constructor.
   { intros h.
@@ -377,8 +393,8 @@ Global Instance issurj_isabelianization {G : Group}
   : IsAbelianization A eta -> IsSurjection eta.
 Proof.
   intros k.
-  pose (homotopic_isabelianization A (abel G) eta (abel_unit G)) as p.
-  refine (@cancelL_isequiv_conn_map _ _ _ _ _ _ _
+  pose (homotopic_isabelianization A (abel G) eta abel_unit) as p.
+  exact (@cancelL_isequiv_conn_map _ _ _ _ _ _ _
     (conn_map_homotopic _ _ _ p _)).
 Defined.
 
diff --git a/theories/Algebra/AbGroups/Biproduct.v b/theories/Algebra/AbGroups/Biproduct.v
index 536f2785df8..4b4c3b047d5 100644
--- a/theories/Algebra/AbGroups/Biproduct.v
+++ b/theories/Algebra/AbGroups/Biproduct.v
@@ -191,8 +191,7 @@ Proof.
   intros h k.
   intros [a b].
   refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^).
-  refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
-  exact (ap011 (+) (h a) (k b)).
+  exact (grp_homo_op_agree f g (h a) (k b)).
 Defined.
 
 (* Maps out of biproducts are determined on the two inclusions. *)
diff --git a/theories/Algebra/AbGroups/Cyclic.v b/theories/Algebra/AbGroups/Cyclic.v
index d8e00f31df6..172984a1f52 100644
--- a/theories/Algebra/AbGroups/Cyclic.v
+++ b/theories/Algebra/AbGroups/Cyclic.v
@@ -48,8 +48,7 @@ Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
 Proof.
   induction n as [|n H].
   1: easy.
-  refine (grp_pow_natural _ _ _ @ _); simpl.
-  by rewrite grp_unit_r.
+  exact (grp_pow_natural _ _ _).
 Defined.
 
 (** [ab_Z1] is projective. *)
@@ -65,8 +64,7 @@ Proof.
   apply path_homomorphism_from_free_group.
   simpl.
   intros [].
-  refine (_ @ a.2).
-  exact (ap p (grp_unit_r _)).
+  exact a.2.
 Defined.
 
 (** The map sending the generator to [1 : Int]. *)
diff --git a/theories/Algebra/AbGroups/FreeAbelianGroup.v b/theories/Algebra/AbGroups/FreeAbelianGroup.v
index 0c897818627..8adeb1f8ddc 100644
--- a/theories/Algebra/AbGroups/FreeAbelianGroup.v
+++ b/theories/Algebra/AbGroups/FreeAbelianGroup.v
@@ -3,6 +3,7 @@ Require Import Types.Sigma Types.Forall Types.Paths.
 Require Import WildCat.Core WildCat.EquivGpd.
 Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Abelianization.
 Require Import Algebra.Groups.FreeGroup.
+Require Import Spaces.List.Core.
 
 (** * Free Abelian Groups *)
 
@@ -29,6 +30,11 @@ Global Instance isfreeabgroup_isfreeabgroupon (S : Type) (F_S : AbGroup) (i : S
 Definition FreeAbGroup (S : Type) : AbGroup
   := abel (FreeGroup S).
 
+Arguments FreeAbGroup S : simpl never.
+
+Definition freeabgroup_in {S : Type} : S -> FreeAbGroup S
+  := abel_unit o freegroup_in.
+
 (** The abelianization of a free group on a set is a free abelian group on that set. *)
 Global Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext}
   {S : Type} {G : Group} {A : AbGroup} (f : S -> G) (g : G $-> A)
@@ -50,6 +56,6 @@ Global Instance isfreeabgroup_freeabgroup `{Funext} (S : Type)
   : IsFreeAbGroup (FreeAbGroup S).
 Proof.
   exists S.
-  exists (abel_unit (FreeGroup S) o freegroup_in).
+  exists (abel_unit (G:=FreeGroup S) o freegroup_in).
   srapply isfreeabgroupon_isabelianization_isfreegroup.
 Defined.
diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v
new file mode 100644
index 00000000000..ced3538649d
--- /dev/null
+++ b/theories/Algebra/AbGroups/TensorProduct.v
@@ -0,0 +1,691 @@
+Require Import Basics.Overture Basics.Tactics.
+Require Import Types.Forall Types.Sigma.
+Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor.
+Require Import WildCat.NatTrans.
+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.
+
+Local Open Scope mc_scope.
+Local Open Scope mc_add_scope.
+
+(** * The Tensor Product of Abelian Groups *)
+
+(** Various maps [A * B → C] from the cartesian product of two abelian groups to another abelian group are "biadditive" (also called "bilinear"), meaning that they are group homomorphisms when we fix the left or right argument.
+
+The tensor product of abelian groups is a construction that produces an abelian group [A ⊗ B] along with a biadditive map [A * B -> A ⊗ B] which is initial among biadditive maps from [A * B].  This means that any biadditive map [A * B → C] factors uniquely through the tensor product via a group homomorphism [A ⊗ B -> C].
+
+Biadditive functions appear in all sorts of contexts ranging from linear algebra to analysis. Therefore having a way to systematically study them is very useful. *)
+
+(** ** Construction *)
+
+(** We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the biadditive pairs. *)
+
+(** Here we define the subgroup of biadditive pairs in two steps. *)
+Definition family_biadditive_pairs {A B : AbGroup}
+  : FreeAbGroup (A * B) -> Type.
+Proof.
+  intros x.
+  refine ((exists (a1 a2 : A) (b : B), _) + exists (a : A) (b1 b2 : B), _)%type. 
+  - refine (- _ + (_ + _) = x).
+    1-3: apply freeabgroup_in.
+    + exact (a1 + a2, b).
+    + exact (a1, b).
+    + exact (a2, b).
+  - refine (- _ + (_ + _) = x).
+    1-3: apply freeabgroup_in.
+    + exact (a, b1 + b2).
+    + exact (a, b1).
+    + exact (a, b2).
+Defined.
+
+Definition subgroup_biadditive_pairs {A B : AbGroup}
+  : Subgroup (FreeAbGroup (A * B))
+  := subgroup_generated family_biadditive_pairs.
+
+(** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to be a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of biadditive pairs. *)
+Definition ab_tensor_prod (A B : AbGroup) : AbGroup
+  := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs.
+
+Arguments ab_tensor_prod A B : simpl never.
+
+(** The tensor product of [A] and [B] contains formal sums and differences of pairs of elements from [A] and [B]. We denote these pairs as "simple tensors" and name them [tensor]. *)
+Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B
+  := fun a b => grp_quotient_map (freeabgroup_in (a, b)).
+
+(** ** Properties of tensors *)
+
+(** The characterizing property of simple tensors are that they are biadditive in their arguments. *)
+
+(** A [tensor] of a sum distributes over the sum on the left. *) 
+Definition tensor_dist_l {A B : AbGroup} (a : A) (b b' : B)
+  : tensor a (b + b') = tensor a b + tensor a b'.
+Proof.
+  apply qglue, tr.
+  apply sgt_in.
+  right.
+  by exists a, b, b'.
+Defined.
+
+(** A [tensor] of a sum distributes over the sum on the right. *)
+Definition tensor_dist_r {A B : AbGroup} (a a' : A) (b : B)
+  : tensor (a + a') b = tensor a b + tensor a' b.
+Proof.
+  apply qglue, tr.
+  apply sgt_in.
+  left.
+  by exists a, a', b.
+Defined.
+
+(** Tensoring on the left is a group homomorphism. *)
+Definition grp_homo_tensor_l {A B : AbGroup} (a : A)
+  : B $-> ab_tensor_prod A B.
+Proof.
+  snrapply Build_GroupHomomorphism.
+  - exact (fun b => tensor a b).
+  - intros b b'.
+    nrapply tensor_dist_l.
+Defined. 
+
+(** Tensoring on the right is a group homomorphism. *)
+Definition grp_homo_tensor_r {A B : AbGroup} (b : B)
+  : A $-> ab_tensor_prod A B.
+Proof.
+  snrapply Build_GroupHomomorphism.
+  - exact (fun a => tensor a b).
+  - intros a a'.
+    nrapply tensor_dist_r.
+Defined.
+
+(** Tensors preserve negation in the left argument. *)
+Definition tensor_neg_l {A B : AbGroup} (a : A) (b : B)
+  : tensor (-a) b = - tensor a b
+  := grp_homo_inv (grp_homo_tensor_r b) a.
+
+(** Tensors preserve negation in the right argument. *)
+Definition tensor_neg_r {A B : AbGroup} (a : A) (b : B)
+  : tensor a (-b) = - tensor a b
+  := grp_homo_inv (grp_homo_tensor_l a) b.
+
+(** Tensoring by zero on the left is zero. *)
+Definition tensor_zero_l {A B : AbGroup} (b : B)
+  : tensor (A:=A) 0 b = 0
+  := grp_homo_unit (grp_homo_tensor_r b).
+
+(** Tensoring by zero on the right is zero. *)
+Definition tensor_zero_r {A B : AbGroup} (a : A)
+  : tensor (B:=B) a 0 = 0
+  := grp_homo_unit (grp_homo_tensor_l a).
+
+(** The [tensor] map is biadditive and therefore can be written in a curried form using the internal abelian group hom. *)
+Definition grp_homo_tensor `{Funext} {A B : AbGroup}
+  : A $-> ab_hom B (ab_tensor_prod A B). 
+Proof.
+  snrapply Build_GroupHomomorphism.
+  - intros a.
+    snrapply Build_GroupHomomorphism.
+    + exact (tensor a).
+    + nrapply tensor_dist_l.
+  - intros a a'.
+    apply equiv_path_grouphomomorphism.
+    intros b.
+    nrapply tensor_dist_r.
+Defined.
+
+(** ** Induction principles *)
+
+(** Here we write down some induction principles to help us prove lemmas about the tensor product. Some of these are quite specialised but are patterns that appear often in practice. *) 
+
+(** Our main recursion principle states that in order to build a homomorphism out of the tensor product, it is sufficient to provide a map out of the direct product which is biadditive, that is, a map that preserves addition in each argument of the product. *)
+
+(** We separate out the proof of this part, so we can make it opaque. *)
+Definition ab_tensor_prod_rec_helper {A B C : AbGroup}
+  (f : A -> B -> C)
+  (l : forall a b b', f a (b + b') = f a b + f a b')
+  (r : forall a a' b, f (a + a') b = f a b + f a' b)
+  (x : FreeAbGroup (A * B)) (insg : subgroup_biadditive_pairs x)
+  : grp_homo_abel_rec (FreeGroup_rec (A * B) C (uncurry f)) x = mon_unit.
+Proof.
+  set (abel_rec := grp_homo_abel_rec (FreeGroup_rec (A * B) C (uncurry f))).
+  strip_truncations.
+  induction insg as [ x biad | | g h insg_g IHg insg_h IHh ].
+  - destruct biad as [ [ a [ a' [ b p ] ] ] | [ a [ b [ b' p ] ] ] ].
+    all: destruct p; simpl.
+    all: apply grp_moveL_M1^-1%equiv; symmetry.
+    1: apply r.
+    apply l.
+  - nrapply grp_homo_unit.
+  - rewrite grp_homo_op, grp_homo_inv.
+    apply grp_moveL_1M^-1.
+    exact (IHg @ IHh^).
+Defined.
+
+Opaque ab_tensor_prod_rec_helper.
+
+Definition ab_tensor_prod_rec {A B C : AbGroup}
+  (f : A -> B -> C)
+  (l : forall a b b', f a (b + b') = f a b + f a b')
+  (r : forall a a' b, f (a + a') b = f a b + f a' b) 
+  : ab_tensor_prod A B $-> C.
+Proof.
+  unfold ab_tensor_prod.
+  snrapply grp_quotient_rec.
+  - snrapply grp_homo_abel_rec.
+    snrapply FreeGroup_rec.
+    exact (uncurry f).
+  - unfold normalsubgroup_subgroup.
+    apply ab_tensor_prod_rec_helper; assumption.
+Defined.
+
+(** We give an induction principle for an hprop-valued type family [P].  It may be surprising at first that we only require [P] to hold for the simple tensors [tensor a b] and be closed under addition.  It automatically follows that [P 0] holds (since [tensor 0 0 = 0]) and that [P] is closed under negation (since [tensor -a b = - tensor a b]). This induction principle says that the simple tensors generate the tensor product as a semigroup. *)
+Definition ab_tensor_prod_ind_hprop {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.
+  - (* The goal here is [P 0], so we use [Hin 0 0 : P (tensor 0 0)]. *)
+    exact (transport P (tensor_zero_l 0) (Hin 0 0)).
+  - change (P (tensor_in (freegroup_eta [a]%list + freegroup_eta w))).
+    (* This [rewrite] is [reflexivity], but the [Defined] is slow if [change] is used instead. *)
+    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))).
+      (* This [rewrite] is also reflexivity. *)
+      rewrite grp_homo_inv.
+      apply Hop; trivial.
+      rewrite <- tensor_neg_l.
+      apply Hin.
+Defined.
+
+(** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing that two group homomorphisms out of the tensor product are homotopic. In order to do this, it suffices to show it only for simple tensors. The homotopy is closed under addition, so we don't need to hypothesise anything else. *)
+Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup}
+  {f f' : ab_tensor_prod A B $-> G}
+  (H : forall a b, f (tensor a b) = f' (tensor a b))
+  : f $== f'.
+Proof.
+  nrapply ab_tensor_prod_ind_hprop.
+  - exact _.
+  - exact H.
+  - intros x y; apply grp_homo_op_agree.
+Defined.
+
+(** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to use this specialised lemma. *)
+Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup}
+  {f f' f'' : ab_tensor_prod A B $-> G}
+  (H : forall a b, f (tensor a b) = f' (tensor a b) + f'' (tensor a b))
+  : forall x, f x = f' x + f'' x
+  := ab_tensor_prod_ind_homotopy (f':=ab_homo_add f' f'') H.
+
+(** Here we give an induction principle for a triple tensor, a.k.a a dependent trilinear function. *)
+Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup}
+  (P : ab_tensor_prod A (ab_tensor_prod B C) -> Type)
+  (H : forall x, IsHProp (P x))
+  (Hin : forall a b c, P (tensor a (tensor b c)))
+  (Hop : forall x y, P x -> P y -> P (x + y))
+  : forall x, P x.
+Proof.
+  rapply (ab_tensor_prod_ind_hprop P).
+  - intros a.
+    rapply (ab_tensor_prod_ind_hprop (fun x => P (tensor _ x))).
+    + nrapply Hin.
+    + intros x y Hx Hy.
+      rewrite tensor_dist_l.
+      by apply Hop.
+  - exact Hop.
+Defined.
+
+(** Similar to before, we specialise the triple tensor induction principle for proving homotopies of trilinear/triadditive functions. *)
+Definition ab_tensor_prod_ind_homotopy_triple {A B C G : AbGroup}
+  {f f' : ab_tensor_prod A (ab_tensor_prod B C) $-> G}
+  (H : forall a b c, f (tensor a (tensor b c)) = f' (tensor a (tensor b c)))
+  : f $== f'.
+Proof.
+  nrapply ab_tensor_prod_ind_hprop_triple.
+  - exact _.
+  - exact H.
+  - intros x y; apply grp_homo_op_agree.
+Defined.
+
+(** As explained for the biadditive and triadditive cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *)
+Definition ab_tensor_prod_ind_hprop_quad {A B C D : AbGroup}
+  (P : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type)
+  (H : forall x, IsHProp (P x))
+  (Hin : forall a b c d, P (tensor a (tensor b (tensor c d))))
+  (Hop : forall x y, P x -> P y -> P (x + y))
+  : forall x, P x.
+Proof.
+  rapply (ab_tensor_prod_ind_hprop P).
+  - intros a.
+    nrapply (ab_tensor_prod_ind_hprop_triple (fun x => P (tensor _ x))).
+    + intro x; apply H.
+    + nrapply Hin.
+    + intros x y Hx Hy.
+      rewrite tensor_dist_l.
+      by apply Hop.
+  - exact Hop.
+Defined.
+
+(** To construct a homotopy between quadrilinear maps we need only check equality for the quadruple simple tensors. *)
+Definition ab_tensor_prod_ind_homotopy_quad {A B C D G : AbGroup}
+  {f f' : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G}
+  (H : forall a b c d, f (tensor a (tensor b (tensor c d)))
+    = f' (tensor a (tensor b (tensor c d))))
+  : f $== f'.
+Proof.
+  nrapply (ab_tensor_prod_ind_hprop_quad (fun _ => _)).
+  - exact _.
+  - exact H.
+  - intros x y; apply grp_homo_op_agree.
+Defined.
+
+(** ** Universal Property of the Tensor Product *)
+
+(** A function of two variables is biadditive if it preserves the operation in each variable. *)
+Class IsBiadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} (f : A -> B -> C) := {
+  isbiadditive_l :: forall b, IsSemiGroupPreserving (flip f b);
+  isbiadditive_r :: forall a, IsSemiGroupPreserving (f a);  
+}.
+
+Definition issig_IsBiadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C}
+  (f : A -> B -> C)
+  : _ <~> IsBiadditive f
+  := ltac:(issig).
+
+(** The truncation level of the [IsBiadditive f] predicate is determined by the truncation level of the codomain. This will almost always be a hset. *)
+Global Instance istrunc_isbiadditive `{Funext}
+  {A B C : Type} `{SgOp A, SgOp B, SgOp C}
+  (f : A -> B -> C) n `{IsTrunc n.+1 C}
+  : IsTrunc n (IsBiadditive f).
+Proof.
+  nrapply istrunc_equiv_istrunc.
+  1: rapply issig_IsBiadditive.
+  unfold IsSemiGroupPreserving.
+  exact _.
+Defined.
+
+(** The simple tensor map is biadditive. *)
+Global Instance isbiadditive_tensor (A B : AbGroup)
+  : IsBiadditive (@tensor A B) := {|
+  isbiadditive_l := fun b a a' => tensor_dist_r a a' b;
+  isbiadditive_r := tensor_dist_l;
+|}.
+
+(** The type of biadditive maps. *)
+Record Biadditive (A B C : Type) `{SgOp A, SgOp B, SgOp C} := {
+  biadditive_fun :> A -> B -> C;
+  biadditive_isbiadditive :: IsBiadditive biadditive_fun;
+}.
+
+Definition issig_Biadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C}
+  : _ <~> Biadditive A B C
+  := ltac:(issig).
+
+(** The universal property of the tensor product is that biadditive maps between abelian groups are in one-to-one corresondance with maps out of the tensor product. In this sense, the tensor product is the most perfect object describing biadditive maps between two abelian groups. *)
+Definition equiv_ab_tensor_prod_rec `{Funext} (A B C : AbGroup)
+  : Biadditive A B C <~> (ab_tensor_prod A B $-> C).
+Proof.
+  snrapply equiv_adjointify.
+  - intros [f [l r]].
+    exact (ab_tensor_prod_rec f r (fun a a' b => l b a a')).
+  - intros f.
+    exists (fun x y => f (tensor x y)).
+    snrapply Build_IsBiadditive.
+    + intros b a a'; simpl.
+      lhs nrapply (ap f).
+      1: nrapply tensor_dist_r.
+      nrapply grp_homo_op.
+    + intros a a' b; simpl.
+      lhs nrapply (ap f).
+      1: nrapply tensor_dist_l.
+      nrapply grp_homo_op.
+  - intros f.
+    snrapply equiv_path_grouphomomorphism.
+    snrapply ab_tensor_prod_ind_homotopy.
+    intros a b; simpl.
+    reflexivity.
+  - intros [f [l r]].
+    snrapply (equiv_ap_inv' issig_Biadditive).
+    rapply path_sigma_hprop; simpl.
+    reflexivity.
+Defined.
+
+(** ** Functoriality of the Tensor Product *)
+
+(** The tensor product produces a bifunctor and we will later show that it gives a symmetric monoidal structure on the category of abelian groups. *)
+
+(** Given a pair of maps, we can produce a homomorphism between the pairwise tensor products of the domains and codomains. *) 
+Definition functor_ab_tensor_prod {A B A' B' : AbGroup}
+  (f : A $-> A') (g : B $-> B')
+  : ab_tensor_prod A B $-> ab_tensor_prod A' B'.
+Proof.
+  snrapply ab_tensor_prod_rec.
+  - intros a b.
+    exact (tensor (f a) (g b)).
+  - intros a b b'; hnf.
+    rewrite grp_homo_op.
+    by rewrite tensor_dist_l.
+  - intros a a' b; hnf.
+    rewrite grp_homo_op.
+    by rewrite tensor_dist_r.
+Defined.
+
+(** 2-functoriality of the tensor product. *)
+Definition functor2_ab_tensor_prod {A B A' B' : AbGroup}
+  {f f' : A $-> A'} (p : f $== f') {g g' : B $-> B'} (q : g $== g')
+  : functor_ab_tensor_prod f g $== functor_ab_tensor_prod f' g'.
+Proof.
+  snrapply ab_tensor_prod_ind_homotopy.
+  intros a b; simpl.
+  exact (ap011 tensor (p _) (q _)).
+Defined.
+
+(** The tensor product functor preserves identity morphisms. *)
+Definition functor_ab_tensor_prod_id (A B : AbGroup)
+  : functor_ab_tensor_prod (Id A) (Id B) $== Id (ab_tensor_prod A B).
+Proof.
+  snrapply ab_tensor_prod_ind_homotopy.
+  intros a b; simpl.
+  reflexivity.
+Defined.
+
+(** The tensor product functor preserves composition. *)
+Definition functor_ab_tensor_prod_compose {A B C A' B' C' : AbGroup}
+  (f : A $-> B) (g : B $-> C) (f' : A' $-> B') (g' : B' $-> C')
+  : functor_ab_tensor_prod (g $o f) (g' $o f')
+    $== functor_ab_tensor_prod g g' $o functor_ab_tensor_prod f f'.
+Proof.
+  snrapply ab_tensor_prod_ind_homotopy.
+  intros a b; simpl.
+  reflexivity.
+Defined.
+
+(** The tensor product functor is a 0-bifunctor. *)
+Global Instance is0bifunctor_ab_tensor_prod : Is0Bifunctor ab_tensor_prod.
+Proof.
+  rapply Build_Is0Bifunctor'.
+  snrapply Build_Is0Functor.
+  intros [A B] [A' B'] [f g].
+  exact (functor_ab_tensor_prod f g).
+Defined.
+
+(** The tensor product functor is a bifunctor. *)
+Global Instance is1bifunctor_ab_tensor_prod : Is1Bifunctor ab_tensor_prod.
+Proof.
+  rapply Build_Is1Bifunctor'.
+  snrapply Build_Is1Functor.
+  - intros AB A'B' fg f'g' [p q].
+    exact (functor2_ab_tensor_prod p q).
+  - intros [A B].
+    exact (functor_ab_tensor_prod_id A B).
+  - intros AA' BB' CC' [f g] [f' g'].
+    exact (functor_ab_tensor_prod_compose f f' g g').
+Defined.
+
+(** ** Symmetry of the Tensor Product *)
+
+(** The tensor product is symmetric in that the order in which we take the tensor shouldn't matter upto isomorphism. *)
+
+(** We can define a swap map which swaps the order of simple tensors. *)
+Definition ab_tensor_swap {A B} : ab_tensor_prod A B $-> ab_tensor_prod B A.
+Proof.
+  snrapply ab_tensor_prod_rec. 
+  - exact (flip tensor).
+  - intros a b b'.
+    apply tensor_dist_r.
+  - intros a a' b.
+    apply tensor_dist_l.
+Defined.
+
+(** [ab_tensor_swap] is involutive. *)
+Definition ab_tensor_swap_swap {A B}
+  : ab_tensor_swap $o @ab_tensor_swap A B $== Id _. 
+Proof.
+  snrapply ab_tensor_prod_ind_homotopy.
+  reflexivity.
+Defined. 
+
+(** [ab_tensor_swap] is natural in both arguments. This means that it also acts on tensor functors. *)
+Definition ab_tensor_swap_natural {A B A' B'} (f : A $-> A') (g : B $-> B')
+  : ab_tensor_swap $o functor_ab_tensor_prod f g
+    $== functor_ab_tensor_prod g f $o ab_tensor_swap.
+Proof.
+  snrapply ab_tensor_prod_ind_homotopy.
+  simpl. (* This speeds up the [reflexivity] and the [Defined]. *)
+  reflexivity.
+Defined.
+
+(** The swap map gives us a symmetric braiding on the category of abelian groups. We will later show it is a full symmetric monoidal category. *)
+Global Instance symmetricbraiding_ab_tensor_prod : SymmetricBraiding ab_tensor_prod.
+Proof.
+  snrapply Build_SymmetricBraiding.
+  - snrapply Build_NatTrans.
+    + intro; exact ab_tensor_swap.
+    + snrapply Build_Is1Natural.
+      intros; nrapply ab_tensor_swap_natural.
+  - intros; nrapply ab_tensor_swap_swap.
+Defined. 
+
+(** ** Twisting Triple Tensors *)
+
+(** In order to construct the symmetric monoidal category, we will use what is termed the "Twist construction" in Monoidal.v. This simplifies the data of a symmetric monoidal category by constructing it from simpler parts. For instance, instead of having to prove full associativity [(A ⊗ B) ⊗ C $-> A ⊗ (B ⊗ C)], we can provide a twist map [A ⊗ (B ⊗ C) $-> B ⊗ (A ⊗ C)] and use the symmetric braiding we have so far to prove associativity. *)
+
+(** In order to be more efficient whilst unfolding definitions, we break up the definition of a twist map into its components. *)
+
+Local Definition ab_tensor_prod_twist_map {A B C : AbGroup}
+  : A -> ab_tensor_prod B C -> ab_tensor_prod B (ab_tensor_prod A C).
+Proof.
+  intros a.
+  snrapply ab_tensor_prod_rec.
+  - intros b c.
+    exact (tensor b (tensor a c)).
+  - intros b c c'; hnf.
+    lhs nrapply ap.
+    1: nrapply tensor_dist_l.
+    nrapply tensor_dist_l.
+  - intros b b' c; hnf.
+    nrapply tensor_dist_r.
+Defined.
+
+Arguments ab_tensor_prod_twist_map {A B C} _ _ /.
+
+Local Definition ab_tensor_prod_twist_map_additive_r {A B C : AbGroup}
+  (a : A) (b b' : ab_tensor_prod B C)
+  : ab_tensor_prod_twist_map a (b + b')
+    = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a b'.
+Proof.
+  intros; nrapply grp_homo_op.
+Defined.
+
+Local Definition ab_tensor_prod_twist_map_additive_l {A B C : AbGroup}
+  (a a' : A) (b : ab_tensor_prod B C)
+  : ab_tensor_prod_twist_map (a + a') b
+    = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a' b.
+Proof.  
+  revert b.
+  nrapply ab_tensor_prod_ind_homotopy_plus.
+  intros b c.
+  change (tensor b (tensor (a + a') c)
+    = tensor b (tensor a c) + tensor b (tensor a' c)). 
+  rhs_V nrapply tensor_dist_l.
+  nrapply (ap (tensor b)).
+  nrapply tensor_dist_r.
+Defined.
+
+(** Given a triple tensor product, we have a twist map which permutes the first two components. *)
+Definition ab_tensor_prod_twist {A B C}
+  : ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C).
+Proof.
+  snrapply ab_tensor_prod_rec.
+  - exact ab_tensor_prod_twist_map. 
+  - exact ab_tensor_prod_twist_map_additive_r.
+  - exact ab_tensor_prod_twist_map_additive_l.
+Defined.
+
+(** The twist map is involutive. *)
+Definition ab_tensor_prod_twist_twist {A B C}
+  : ab_tensor_prod_twist $o @ab_tensor_prod_twist A B C $== Id _.
+Proof.
+  snrapply ab_tensor_prod_ind_homotopy_triple.
+  reflexivity.
+Defined.
+
+(** The twist map is natural in all 3 arguments. This means that the twist map acts on the triple tensor functor in the same way. *)
+Definition ab_tensor_prod_twist_natural {A B C A' B' C'}
+  (f : A $-> A') (g : B $-> B') (h : C $-> C')
+  : ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h)
+    $== fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ab_tensor_prod_twist.
+Proof.
+  snrapply ab_tensor_prod_ind_homotopy_triple.
+  intros a b c.
+  (* This [change] speeds up the [reflexivity].  [simpl] produces a goal that looks the same, but is still slow. *)
+  change (tensor (g b) (tensor (f a) (h c)) = tensor (g b) (tensor (f a) (h c))).
+  reflexivity.
+Defined.
+
+(** ** Unitality of [abgroup_Z] *)
+
+(** In the symmetric monoidal structure on abelian groups, [abgroup_Z] is the unit. We show that tensoring with [abgroup_Z] on the right is isomorphic to the original group. *)
+
+(** First we characterise the action of integers via [grp_pow] and their interaction on tensors. This is just a generalisation of the distributivity laws for tensors. *)
+
+(** Multiplication in the first factor can be factored out. *)
+Definition tensor_ab_mul_l {A B : AbGroup} (z : Int) (a : A) (b : B)
+  : tensor (ab_mul z a) b = ab_mul z (tensor a b)
+  := ab_mul_natural (grp_homo_tensor_r b) z a.
+
+(** Multiplication in the second factor can be factored out. *)
+Definition tensor_ab_mul_r {A B : AbGroup} (z : Int) (a : A) (b : B)
+  : tensor a (ab_mul z b) = ab_mul z (tensor a b)
+  := ab_mul_natural (grp_homo_tensor_l a) z b.
+
+(** Multiplication can be transferred from one factor to the other. The tensor product of [R]-modules will include this as an extra axiom, but here we have [Z]-modules and we can prove it. *)
+Definition tensor_ab_mul {A B : AbGroup} (z : Int) (a : A) (b : B)
+  : tensor (ab_mul z a) b = tensor a (ab_mul z b).
+Proof.
+  rhs nrapply tensor_ab_mul_r.
+  nrapply tensor_ab_mul_l.
+Defined.
+
+(** [abgroup_Z] is a right identity for the tensor product. *) 
+Definition ab_tensor_prod_Z_r {A}
+  : ab_tensor_prod A abgroup_Z $<~> A.
+Proof.
+  (** Checking that the inverse map is a homomorphism is easier. *)
+  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 z z'; cbn beta.
+        nrapply grp_homo_op.
+      * 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.
+
+(** We have a right unitor for the tensor product given by unit [abgroup_Z]. Naturality of [ab_tensor_prod_Z_r] is straightforward to prove. *)
+Global Instance rightunitor_ab_tensor_prod
+  : RightUnitor ab_tensor_prod abgroup_Z.
+Proof.
+  snrapply Build_NatEquiv.
+  - intros A.
+    apply ab_tensor_prod_Z_r.
+  - snrapply Build_Is1Natural.
+    intros A A' f.
+    snrapply ab_tensor_prod_ind_homotopy.
+    intros a z.
+    change (grp_pow (f a) z = f (grp_pow a z)).
+    exact (grp_pow_natural _ _ _)^.
+Defined.
+
+(** Since we have symmetry of the tensor product, we get left unitality for free. *)
+Global Instance left_unitor_ab_tensor_prod
+  : LeftUnitor ab_tensor_prod abgroup_Z.
+Proof.
+  rapply left_unitor_twist.
+Defined.
+
+(** ** Symmetric Monoidal Structure of Tensor Product *)
+
+(** Using the twist construction we can derive an associator for the tensor product. In other words, we have associativity of the tensor product of abelian groups natural in each factor. *)
+Global Instance associator_ab_tensor_prod : Associator ab_tensor_prod.
+Proof.
+  srapply associator_twist.
+  - exact @ab_tensor_prod_twist.
+  - intros; nrapply ab_tensor_prod_twist_twist.
+  - intros; nrapply ab_tensor_prod_twist_natural.
+Defined.
+
+(** The triangle identity is straightforward to prove using the custom induction principles we proved earlier. *)
+Global Instance triangle_ab_tensor_prod
+  : TriangleIdentity ab_tensor_prod abgroup_Z.
+Proof.
+  snrapply triangle_twist.
+  intros A B.
+  snrapply ab_tensor_prod_ind_homotopy_triple.
+  intros a b z.
+  exact (tensor_ab_mul z a b)^.
+Defined.
+
+(** The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle. *)
+Global Instance hexagon_ab_tensor_prod : HexagonIdentity ab_tensor_prod.
+Proof.
+  snrapply hexagon_twist.
+  intros A B C.
+  snrapply ab_tensor_prod_ind_homotopy_triple.
+  intros b a c.
+  change (tensor c (tensor a b) = tensor c (tensor a b)).
+  reflexivity.
+Defined.
+
+(** Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the simple tensor redexes. *)
+Global Instance pentagon_ab_tensor_prod : PentagonIdentity ab_tensor_prod.
+Proof.
+  snrapply pentagon_twist.
+  intros A B C D.
+  snrapply ab_tensor_prod_ind_homotopy_quad.
+  intros a b c d.
+  change (tensor c (tensor d (tensor a b)) = tensor c (tensor d (tensor a b))). 
+  reflexivity.
+Defined.
+
+(** We therefore have all the data of a monoidal category. *)
+Global Instance ismonoidal_ab_tensor_prod
+  : IsMonoidal AbGroup ab_tensor_prod abgroup_Z
+  := {}.
+
+(** And furthermore, all the data of a symmetric monoidal category. *)
+Global Instance issymmmetricmonoidal_ab_tensor_prod
+  : IsSymmetricMonoidal AbGroup ab_tensor_prod abgroup_Z
+  := {}.
+
+(** 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/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index d476119a3f1..c8a31d9eec2 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -22,7 +22,7 @@ Proof.
   - exact int_add_comm.
 Defined.
 
-(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. *)
+(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism.  See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *)
 Definition grp_pow_homo {G : Group} (g : G)
   : GroupHomomorphism abgroup_Z G.
 Proof.
@@ -30,3 +30,21 @@ Proof.
   1: exact (grp_pow g).
   intros m n; apply grp_pow_add.
 Defined.
+
+Local Open Scope mc_add_scope.
+
+(** [ab_mul] (and [grp_pow]) give multiplication in [abgroup_Z]. *)
+Definition abgroup_Z_ab_mul (z z' : Int)
+  : ab_mul (A:=abgroup_Z) z z' = z * z'.
+Proof.
+  induction z.
+  - reflexivity.
+  - cbn.
+    lhs nrapply (grp_pow_succ (G:=abgroup_Z)).
+    rhs nrapply int_mul_succ_l.
+    f_ap.
+  - cbn.
+    lhs nrapply (grp_pow_pred (G:=abgroup_Z)).
+    rhs nrapply int_mul_pred_l.
+    f_ap.
+Defined.
diff --git a/theories/Algebra/AbSES/Pushout.v b/theories/Algebra/AbSES/Pushout.v
index 022f02b7979..ea70463902b 100644
--- a/theories/Algebra/AbSES/Pushout.v
+++ b/theories/Algebra/AbSES/Pushout.v
@@ -85,7 +85,7 @@ Proof.
     1: apply issurj_class_of.
     2: exact _.
     intro x; simpl.
-    refine (grp_homo_op (projection F) _ _ @ ap011 (+) _ _ @ (grp_homo_op _ _ _ )^).
+    nrapply grp_homo_op_agree.
     + refine (_ @ (grp_homo_unit _)^).
       apply iscomplex_abses.
     + apply right_square.
diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v
index 0e5c23c360f..a0c8a5954d1 100644
--- a/theories/Algebra/Groups/FreeGroup.v
+++ b/theories/Algebra/Groups/FreeGroup.v
@@ -14,6 +14,8 @@ Section Reduction.
 
   Universe u.
   Context (A : Type@{u}).
+  
+  Local Open Scope list_scope.
 
   (** We define words (with inverses) on A to be lists of marked elements of A *)
   Local Definition Words : Type@{u} := list (A + A).
@@ -22,7 +24,7 @@ Section Reduction.
   Local Definition change_sign : A + A -> A + A := equiv_sum_symm A A.
 
   (** We introduce a local notation for [change_sign]. It is only defined in this section however. *)
-  Local Notation "x ^" := (change_sign x).
+  Local Notation "a ^" := (change_sign a).
 
   (** Changing sign is an involution *)
   Local Definition change_sign_inv a : a^^ = a.
@@ -30,48 +32,30 @@ Section Reduction.
     by destruct a.
   Defined.
 
-  (** We can concatenate words using list concatenation *)
-  Local Definition word_concat : Words -> Words -> Words := @app _.
-
-  (** We introduce a local notation for word_concat. *)
-  Local Infix "@" := word_concat.
-
-  Local Definition word_concat_w_nil x : x @ nil = x.
-  Proof.
-    induction x; trivial.
-    cbn; f_ap.
-  Defined.
-
-  Local Definition word_concat_w_ww x y z : x @ (y @ z) = (x @ y) @ z.
-  Proof.
-    apply app_assoc.
-  Defined.
-
-  (** Singleton word *)
-  Local Definition word_sing (x : A + A) : Words := (cons x nil).
-
-  Local Notation "[ x ]" := (word_sing x).
-
   (** Now we wish to define the free group on A as the following HIT: 
 
     HIT N(A) : hSet
      | eta : Words -> N(A)
      | tau (x : Words) (a : A + A) (y : Words)
-         : eta (x @ [a] @ [a^] @ y) = eta (x @ y).
+         : eta (x ++ [a] ++ [a^] ++ y) = eta (x ++ y).
 
     Since we cannot write our HITs directly like this (without resorting to private inductive types), we will construct this HIT out of HITs we know. In fact, we can define N(A) as a coequalizer. *)
 
   Local Definition map1 : Words * (A + A) * Words -> Words.
   Proof.
     intros [[x a] y].
-    exact (x @ [a] @ [a^] @ y).
+    exact (x ++ [a] ++ [a^] ++ y).
   Defined.
+  
+  Arguments map1 _ /.
 
   Local Definition map2 : Words * (A + A) * Words -> Words.
   Proof.
     intros [[x a] y].
-    exact (x @ y).
+    exact (x ++ y).
   Defined.
+  
+  Arguments map2 _ /.
 
   (** Now we can define the underlying type of the free group as the 0-truncated coequalizer of these two maps *)
   Definition freegroup_type : Type := Tr 0 (Coeq map1 map2).
@@ -81,7 +65,7 @@ Section Reduction.
 
   (** This is the path constructor *)
   Definition freegroup_tau (x : Words) (a : A + A) (y : Words)
-    : freegroup_eta (x @ [a] @ [a^] @ y) = freegroup_eta (x @ y).
+    : freegroup_eta (x ++ [a] ++ [a^] ++ y) = freegroup_eta (x ++ y).
   Proof.
     apply path_Tr, tr.
     exact ((cglue (x, a, y))).
@@ -96,87 +80,87 @@ Section Reduction.
     { intros x; revert y.
       snrapply Coeq_rec.
       { intros y.
-        exact (freegroup_eta (x @ y)). }
-      intros [[y a] z]; cbn.
-      refine (concat (ap _ _) _).
-      { refine (concat (word_concat_w_ww _ _ _) _).
-        rapply (ap (fun t => t @ _)).
-        refine (concat (word_concat_w_ww _ _ _) _).
-        rapply (ap (fun t => t @ _)).
-        refine (word_concat_w_ww _ _ _). }
-      refine (concat _ (ap _ _^)).
-      2: apply word_concat_w_ww.
-      apply freegroup_tau. }
+        exact (freegroup_eta (x ++ y)). }
+      intros [[y a] z]; simpl.
+      change (freegroup_eta (x ++ y ++ ([a] ++ [a^] ++ z))
+        = freegroup_eta (x ++ y ++ z)).
+      rhs nrapply ap.
+      2: nrapply app_assoc.
+      lhs nrapply ap.
+      1: nrapply app_assoc.
+      nrapply (freegroup_tau _ a). }
     intros [[c b] d].
-    simpl.
     revert y.
     snrapply Coeq_ind.
-    { simpl.
-      intro a.
-      rewrite <- word_concat_w_ww.
-      rewrite <- (word_concat_w_ww _ _ a).
-      rapply (freegroup_tau c b (d @ a)). }
-    intro; rapply path_ishprop.
+    2: intro; rapply path_ishprop. 
+    intro a.
+    change (freegroup_eta ((c ++ [b] ++ [b^] ++ d) ++ a)
+      = freegroup_eta ((c ++ d) ++ a)).
+    lhs_V nrapply ap.
+    1: nrapply app_assoc.
+    lhs_V nrapply (ap (fun x => freegroup_eta (c ++ x))).
+    1: nrapply app_assoc.
+    lhs_V nrapply (ap (fun x => freegroup_eta (c ++ _ ++ x))).
+    1: nrapply app_assoc.
+    rhs_V nrapply ap.
+    2: nrapply app_assoc.
+    nrapply freegroup_tau.
   Defined.
 
   (** The unit of the free group is the empty word *)
-  Global Instance monunit_freegroup_type : MonUnit freegroup_type.
-  Proof.
-    apply freegroup_eta.
-    exact nil.
-  Defined.
+  Global Instance monunit_freegroup_type : MonUnit freegroup_type
+    := freegroup_eta nil.
 
   (** We can change the sign of all the elements in a word and reverse the order. This will be the inversion in the group *)
-  Fixpoint word_change_sign (x : Words) : Words.
-  Proof.
-    destruct x as [|x xs].
-    1: exact nil.
-    exact (word_change_sign xs @ [change_sign x]).
-  Defined.
+  Definition word_change_sign (x : Words) : Words
+    := reverse (list_map change_sign x).
 
   (** Changing the sign changes the order of word concatenation *)
   Definition word_change_sign_ww (x y : Words)
-    : word_change_sign (x @ y) = word_change_sign y @ word_change_sign x.
+    : word_change_sign (x ++ y) = word_change_sign y ++ word_change_sign x.
   Proof.
-    induction x.
-    { symmetry.
-      apply word_concat_w_nil. }
-    simpl.
-    refine (concat _ (inverse (word_concat_w_ww _ _ _))).
-    f_ap.
+    unfold word_change_sign.
+    lhs nrapply (ap reverse).
+    1: nrapply list_map_app.
+    nrapply reverse_app.
   Defined.
 
   (** This is also involutive *)
   Lemma word_change_sign_inv x : word_change_sign (word_change_sign x) = x.
   Proof.
-    induction x.
-    1: reflexivity.
-    simpl.
-    rewrite word_change_sign_ww.
-    cbn; f_ap.
+    unfold word_change_sign.
+    lhs_V nrapply list_map_reverse.
+    lhs nrapply ap.
+    1: nrapply reverse_reverse. 
+    lhs_V nrapply list_map_compose.
+    snrapply list_map_id.
+    intros a ?.
     apply change_sign_inv.
   Defined.
 
   (** Changing the sign gives us left inverses *)
-  Lemma word_concat_Vw x : freegroup_eta (word_change_sign x @ x) = mon_unit.
+  Lemma word_concat_Vw x : freegroup_eta (word_change_sign x ++ x) = mon_unit.
   Proof.
     induction x.
     1: reflexivity.
-    simpl.
+    lhs nrapply (ap (fun x => freegroup_eta (x ++ _))).
+    1: nrapply reverse_cons.
+    change (freegroup_eta ((word_change_sign x ++ [a^]) ++ [a] ++ x)
+      = mon_unit). 
+    lhs_V nrapply ap.
+    1: nrapply app_assoc.
     set (a' := a^).
     rewrite <- (change_sign_inv a).
-    change (freegroup_eta ((word_change_sign x @ [a']) @ ([a'^] @ x)) = mon_unit).
-    rewrite word_concat_w_ww.
-    rewrite freegroup_tau.
+    lhs nrapply freegroup_tau.
     apply IHx.
   Defined.
 
   (** And since changing the sign is involutive we get right inverses from left inverses *)
-  Lemma word_concat_wV x : freegroup_eta (x @ word_change_sign x) = mon_unit.
+  Lemma word_concat_wV x : freegroup_eta (x ++ word_change_sign x) = mon_unit.
   Proof.
     set (x' := word_change_sign x).
     rewrite <- (word_change_sign_inv x).
-    change (freegroup_eta (word_change_sign x' @ x') = mon_unit).
+    change (freegroup_eta (word_change_sign x' ++ x') = mon_unit).
     apply word_concat_Vw.
   Defined.
 
@@ -191,21 +175,20 @@ Section Reduction.
       exact (word_change_sign x). }
     intros [[b a] c].
     unfold map1, map2.
-    refine (concat _ (ap _ (inverse _))).
-    2: apply word_change_sign_ww.
-    refine (concat (ap _ _) _).
-    { refine (concat (word_change_sign_ww _ _) _).
-      apply ap.
-      refine (concat (ap _ (inverse (word_concat_w_ww _ _ _))) _).
-      refine (concat (word_change_sign_ww _ _) _).
-      rapply (ap (fun t => t @ word_change_sign b)).
-      apply word_change_sign_ww. }
-    refine (concat _ (freegroup_tau _ a _)).
-    apply ap.
-    refine (concat (word_concat_w_ww _ _ _) _); f_ap.
-    refine (concat (word_concat_w_ww _ _ _) _); f_ap.
-    f_ap; cbn; f_ap.
-    apply change_sign_inv.
+    lhs nrapply ap.
+    { lhs nrapply word_change_sign_ww.
+      nrapply (ap (fun x => x ++ _)). 
+      lhs nrapply word_change_sign_ww.
+      nrapply (ap (fun x => x ++ _)). 
+      lhs nrapply word_change_sign_ww.
+      nrapply (ap (fun x => _ ++ x)).
+      nrapply (word_change_sign_inv [a]). }
+    lhs_V nrapply ap.
+    1: rhs_V nrapply app_assoc.
+    1: nrapply app_assoc.
+    rhs nrapply ap.
+    2: nrapply word_change_sign_ww.
+    nrapply freegroup_tau.
   Defined.
 
   (** Now we can start to prove the group laws. Since these are hprops we can ignore what happens with the path constructor. *)
@@ -218,8 +201,8 @@ Section Reduction.
     revert x; snrapply Coeq_ind; intro x; [ | apply path_ishprop].
     revert y; snrapply Coeq_ind; intro y; [ | apply path_ishprop].
     revert z; snrapply Coeq_ind; intro z; [ | apply path_ishprop].
-    rapply (ap (tr o coeq)).
-    apply word_concat_w_ww.
+    nrapply (ap (tr o coeq)).
+    nrapply app_assoc.
   Defined.
 
   (** Left identity *)
@@ -236,7 +219,7 @@ Section Reduction.
     rapply Trunc_ind.
     srapply Coeq_ind; intro x; [ | apply path_ishprop].
     apply (ap tr), ap.
-    apply word_concat_w_nil.
+    nrapply app_nil.
   Defined.
 
   (** Left inverse *)
@@ -260,43 +243,66 @@ Section Reduction.
   Proof.
     snrapply (Build_Group freegroup_type); repeat split; exact _.
   Defined.
+  
+  Definition word_rec (G : Group) (s : A -> G) : A + A -> G.
+  Proof.
+    intros [x|x].
+    - exact (s x).
+    - exact (- s x).
+  Defined.
 
+  (** When we have a list of words we can recursively define a group element. The obvious choice would be to map [nil] to the identity and [x :: xs] to [x * words_rec xs]. This has the disadvantage that a single generating element gets mapped to [x * 1] instead of [x]. To fix this issue, we map [nil] to the identity, the singleton to the element we want, and do the rest recursively. *)
   Definition words_rec (G : Group) (s : A -> G) : Words -> G.
   Proof.
-    intro x.
-    induction x as [|x xs].
-    1: exact mon_unit.
-    refine (_ * IHxs).
-    destruct x as [x|x].
-    1: exact (s x).
-    exact (- s x).
+    intro xs.
+    induction xs as [|x [|y xs] IHxs].
+    - exact mon_unit.
+    - exact (word_rec G s x).
+    - exact (word_rec G s x * IHxs).
+  Defined.
+
+  Definition words_rec_cons (G : Group) (s : A -> G) (x : A + A) (xs : Words)
+    : words_rec G s (x :: xs)%list = word_rec G s x * words_rec G s xs.
+  Proof.
+    induction xs in x |- *.
+    - symmetry; nrapply grp_unit_r.
+    - reflexivity.
   Defined.
 
   Lemma words_rec_pp (G : Group) (s : A -> G)  (x y : Words)
-    : words_rec G s (x @ y) = words_rec G s x * words_rec G s y.
+    : words_rec G s (x ++ y) = words_rec G s x * words_rec G s y.
   Proof.
-    induction x.
-    1: symmetry; apply left_identity.
-    cbn; rewrite <- simple_associativity.
-    f_ap.
+    induction x as [|x xs IHxs] in y |- *.
+    - symmetry; nrapply grp_unit_l.
+    - change ((?x :: ?xs) ++ y) with (x :: xs ++ y).
+      lhs nrapply words_rec_cons.
+      lhs nrapply ap.
+      1: nrapply IHxs.
+      lhs nrapply grp_assoc.
+      nrapply (ap (.* _)).
+      symmetry.
+      apply words_rec_cons.
   Defined.
 
   Lemma words_rec_coh (G : Group) (s : A -> G) (a : A + A) (b c : Words)
     : words_rec G s (map1 (b, a, c)) = words_rec G s (map2 (b, a, c)).
   Proof.
     unfold map1, map2.
-    refine (concat _ (words_rec_pp G s _ _)^).
-    refine (concat (words_rec_pp G s _ _) _); f_ap.
-    refine (concat _ (right_identity _)).
-    refine (concat (ap _ (word_concat_w_ww _ _ _)^) _).
-    refine (concat (words_rec_pp G s _ _) _); f_ap.
-    refine (concat (concat (simple_associativity _ _ _) _) (left_identity mon_unit)).
-    destruct a; simpl; f_ap.
-    + apply right_inverse.
-    + apply left_inverse.
+    rhs nrapply (words_rec_pp G s).
+    lhs nrapply words_rec_pp.
+    nrapply (ap (_ *.)).
+    lhs nrapply words_rec_pp.
+    lhs nrapply ap.
+    1: nrapply words_rec_pp.
+    lhs nrapply grp_assoc.
+    rhs_V nrapply grp_unit_l.
+    nrapply (ap (.* _)).
+    destruct a; simpl.
+    - nrapply grp_inv_r.
+    - nrapply grp_inv_l.
   Defined.
 
-  (** Given a group [G] we can construct a group homomorphism [FreeGroup A -> G] if we have a map [A -> G] *)
+  (** Given a group [G] we can construct a group homomorphism [FreeGroup A -> G] if we have a map [A -> G]. *)
   Definition FreeGroup_rec (G : Group) (s : A -> G)
     : GroupHomomorphism FreeGroup G.
   Proof.
@@ -313,51 +319,83 @@ Section Reduction.
     apply words_rec_pp.
   Defined.
 
+  Definition freegroup_in : A -> FreeGroup
+    := freegroup_eta o (fun x => [ x ]) o inl.
+
+  Definition FreeGroup_rec_beta {G : Group} (f : A -> G)
+    : FreeGroup_rec _ f o freegroup_in == f
+    := fun _ => idpath.
+
+  Coercion freegroup_in : A >-> group_type.
+  
+  Definition FreeGroup_ind_hprop' (P : FreeGroup -> Type)
+    `{forall x, IsHProp (P x)}
+    (H1 : forall w, P (freegroup_eta w))
+    : forall x, P x.
+  Proof.
+    rapply Trunc_ind.
+    snrapply Coeq_ind.
+    - exact H1.
+    - intro; apply path_ishprop.
+  Defined.
+ 
+  Definition FreeGroup_ind_hprop (P : FreeGroup -> Type)
+    `{forall x, IsHProp (P x)}
+    (H1 : P mon_unit)
+    (Hin : forall x, P (freegroup_in x))
+    (Hop : forall x y, P x -> P y -> P (- x * y))
+    : forall x, P x.
+  Proof.
+    rapply FreeGroup_ind_hprop'.
+    intros w.
+    induction w as [|a w IHw].
+    - exact H1.
+    - destruct a as [a|a].
+      + change (P ((freegroup_in a) * freegroup_eta w)).  
+        rewrite <- (grp_inv_inv a).
+        apply Hop.
+        * rewrite <- grp_unit_r.
+          by apply Hop.
+        * assumption.
+      + change (P (-(freegroup_in a) * freegroup_eta w)).
+        by apply Hop.
+  Defined.
+  
+  Definition FreeGroup_ind_homotopy {G : Group} {f f' : FreeGroup $-> G}
+    (H : forall x, f (freegroup_in x) = f' (freegroup_in x))
+    : f $== f'.
+  Proof.
+    rapply FreeGroup_ind_hprop.
+    - exact (concat (grp_homo_unit f) (grp_homo_unit f')^).
+    - exact H.
+    - intros x y p q. refine (grp_homo_op_agree f f' _ q).
+      lhs nrapply grp_homo_inv.
+      rhs nrapply grp_homo_inv.
+      exact (ap _ p).
+  Defined.
+
   (** Now we need to prove that the free group satisifes the unviersal property of the free group. *)
   (** TODO: remove funext from here and universal property of free group *)
   Global Instance isfreegroupon_freegroup `{Funext}
-    : IsFreeGroupOn A FreeGroup (freegroup_eta o word_sing o inl).
+    : IsFreeGroupOn A FreeGroup freegroup_in.
   Proof.
     intros G f.
     snrapply Build_Contr.
     { srefine (_;_); simpl.
       1: apply FreeGroup_rec, f.
-      intro x; simpl.
-      apply right_identity. }
+      intro x; reflexivity. }
     intros [g h].
     nrapply path_sigma_hprop; [ exact _ |].
     simpl.
     apply equiv_path_grouphomomorphism.
-    intro x.
-    rewrite <- (path_forall _ _ h).
-    strip_truncations; revert x.
-    snrapply Coeq_ind; intro x; [|apply path_ishprop].
-    hnf; symmetry.
-    induction x.
-    1: apply (grp_homo_unit g).
-    refine (concat (grp_homo_op g (freegroup_eta [a]) (freegroup_eta x)) _).
-    simpl.
-    f_ap.
-    destruct a.
-    1: reflexivity.
-    exact (grp_homo_inv g (freegroup_eta [inl a])).
+    symmetry.
+    snrapply FreeGroup_ind_homotopy.
+    exact h.
   Defined.
 
   (** Typeclass search can already find this but we leave it here as a definition for reference. *)
   Definition isfreegroup_freegroup `{Funext} : IsFreeGroup FreeGroup := _.
 
-  Definition freegroup_in : A -> FreeGroup
-    := freegroup_eta o word_sing o inl.
-
-  Lemma FreeGroup_rec_beta {G : Group} (f : A -> G)
-    : FreeGroup_rec _ f o freegroup_in == f.
-  Proof.
-    intros x.
-    apply grp_unit_r.
-  Defined.
-
-  Coercion freegroup_in : A >-> group_type.
-
 End Reduction.
 
 Arguments freegroup_eta {A}.
diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v
index 7dfc1063fb6..ff9795fdda7 100644
--- a/theories/Algebra/Groups/FreeProduct.v
+++ b/theories/Algebra/Groups/FreeProduct.v
@@ -732,8 +732,8 @@ Proof.
     1: exact (grp_homo_unit _ @ (grp_homo_unit _)^).
     Local Notation "[ x ]" := (cons x nil).
     change (f (amal_eta [gh] * amal_eta w) = g (amal_eta [gh] * amal_eta w)).
-    refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
-    f_ap; clear IHw w.
+    nrapply grp_homo_op_agree.
+    2: apply IHw.
     destruct gh as [g' | h].
     + exact (p g').
     + exact (q h).
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 4a9c8866337..7c63afba058 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -480,6 +480,29 @@ Section GroupMovement.
 
 End GroupMovement.
 
+(** ** Commutation *)
+
+(** If [g] commutes with [h], then [g] commutes with the inverse [-h]. *)
+Definition grp_commutes_inv {G : Group} (g h : G) (p : g * h = h * g)
+  : g * (-h) = (-h) * g.
+Proof.
+  apply grp_moveR_gV.
+  rhs_V apply simple_associativity.
+  by apply grp_moveL_Vg.
+Defined.
+
+(** If [g] commutes with [h] and [h'], then [g] commutes with their product [h * h']. *)
+Definition grp_commutes_op {G : Group} (g h h' : G)
+  (p : g * h = h * g) (p' : g * h' = h' * g)
+  : g * (h * h') = (h * h') * g.
+Proof.
+  lhs apply simple_associativity.
+  lhs nrapply (ap (.* h') p).
+  lhs_V apply simple_associativity.
+  lhs nrapply (ap (h *.) p').
+  by apply simple_associativity.
+Defined.
+
 (** ** Power operation *)
 
 (** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *)
@@ -541,6 +564,28 @@ Proof.
   - reflexivity.
 Defined.
 
+(** If [h] commutes with [g], then [h] commutes with [grp_pow g n]. *)
+Definition grp_pow_commutes {G : Group} (n : Int) (g h : G)
+  (p : h * g = g * h)
+  : h * (grp_pow g n) = (grp_pow g n) * h.
+Proof.
+  induction n.
+  - exact (grp_unit_r _ @ (grp_unit_l _)^).
+  - rewrite grp_pow_succ.
+    nrapply grp_commutes_op; assumption.
+  - rewrite grp_pow_pred.
+    nrapply grp_commutes_op.
+    2: assumption.
+    apply grp_commutes_inv, p.
+Defined.
+
+(** [grp_pow g n] commutes with [g]. *)
+Definition grp_pow_commutes' {G : Group} (n : Int) (g : G)
+  : g * grp_pow g n = grp_pow g n * g.
+Proof.
+  by apply grp_pow_commutes.
+Defined.
+
 (** ** The category of Groups *)
 
 (** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *)
@@ -928,3 +973,13 @@ Proof.
   refine (ap f _).
   apply C.
 Defined.
+
+(** If two group homomorphisms agree on two elements, then they agree on their product. *)
+Definition grp_homo_op_agree {G G' H : Group} (f : G $-> H) (f' : G' $-> H)
+  {x y : G} {x' y' : G'} (p : f x = f' x') (q : f y = f' y')
+  : f (x * y) = f' (x' * y').
+Proof.
+  lhs nrapply grp_homo_op.
+  rhs nrapply grp_homo_op.
+  exact (ap011 _ p q).
+Defined.
diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v
index 92d1d1a8b80..42f009caf9b 100644
--- a/theories/Algebra/Groups/GroupCoeq.v
+++ b/theories/Algebra/Groups/GroupCoeq.v
@@ -42,7 +42,7 @@ Proof.
     simpl.
     destruct a as [a|a].
     1,2: refine (ap _ (grp_homo_op _ _ _) @ _).
-    1,2: refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^); f_ap.
+    1,2: nrapply grp_homo_op_agree; trivial.
     symmetry.
     apply p. }
   { intros [k p] x.
diff --git a/theories/Algebra/Groups/GrpPullback.v b/theories/Algebra/Groups/GrpPullback.v
index c3c3dca73c3..13b19e43bc3 100644
--- a/theories/Algebra/Groups/GrpPullback.v
+++ b/theories/Algebra/Groups/GrpPullback.v
@@ -16,9 +16,7 @@ Section GrpPullback.
   Proof.
     intros [b [c p]] [d [e q]].
     refine (b * d; c * e; _).
-    refine (grp_homo_op f b d @ (_ @ _) @ (grp_homo_op g c e)^).
-    - exact (ap (fun y:A => f b * y) q).
-    - exact (ap (fun x:A => x * g e) p).
+    exact (grp_homo_op_agree _ _ p q).
   Defined.
 
   Local Instance grp_pullback_sgop_associative
diff --git a/theories/Algebra/Groups/Presentation.v b/theories/Algebra/Groups/Presentation.v
index 18d99526b76..0a1a7b2b182 100644
--- a/theories/Algebra/Groups/Presentation.v
+++ b/theories/Algebra/Groups/Presentation.v
@@ -3,7 +3,7 @@ Require Import Truncations.Core.
 Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.FreeGroup.
 Require Import Algebra.Groups.GroupCoeq.
-Require Import Spaces.Finite.
+Require Import Spaces.Finite Spaces.List.Core.
 Require Import WildCat.
 
 
@@ -92,32 +92,13 @@ Proof.
   intros f.
   srapply equiv_iff_hprop.
   { intros p.
-    hnf.
-    rapply Trunc_ind.
-    srapply Coeq.Coeq_ind.
-    2: intros; apply path_ishprop.
-    intros w; hnf.
-    induction w.
-    1: reflexivity.
-    simpl.
-    refine (_ @ _ @ _^).
-    1,3: exact (grp_homo_op (FreeGroup_rec _ _ _) _ _).
-    f_ap.
-    destruct a.
-    1: refine (p _ @ (grp_homo_unit _)^).
-    refine (grp_homo_inv _ _ @ ap _ _ @ (grp_homo_inv _ _)^).
-    refine (p _ @ (grp_homo_unit _)^). }
+    change (equiv_freegroup_rec H _ f $o FreeGroup_rec _ _ (gp_relators P)
+      $== equiv_freegroup_rec _ _ f $o FreeGroup_rec _ _ (fun _ => group_unit)).
+    rapply FreeGroup_ind_homotopy.
+    exact p. }
   intros p r.
   hnf in p.
-  pose (p' := p o freegroup_eta).
-  clearbody p'; clear p.
-  specialize (p' (FreeGroup.word_sing _ (inl r))).
-  refine (_ @ p').
-  clear p'.
-  symmetry.
-  refine (grp_homo_op _ _ _ @ _).
-  refine (_ @ right_identity _).
-  f_ap.
+  exact (p (freegroup_in r)).
 Defined.
 
 (** ** Constructors for finite presentations *)
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index 802a6ff18d7..41ea9e6104a 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -150,22 +150,30 @@ Section QuotientGroup.
     - srapply Quotient_rec.
       + exact f.
       + cbn; intros x y n.
-        symmetry.
-        apply grp_moveL_M1.
-        rewrite <- grp_homo_inv.
-        rewrite <- grp_homo_op.
-        apply h; assumption.
+        apply grp_moveR_M1.
+        rhs_V nrapply (ap (.* f y) (grp_homo_inv _ _)).
+        rhs_V nrapply grp_homo_op.
+        symmetry; apply h; assumption.
     - intro x.
       refine (Quotient_ind_hprop _ _ _).
       intro y. revert x.
-
       refine (Quotient_ind_hprop _ _ _).
       intro x; simpl.
       apply grp_homo_op.
   Defined.
 
+  Definition grp_quotient_ind_hprop (P : QuotientGroup -> Type)
+    `{forall x, IsHProp (P x)}
+    (H1 : forall x, P (grp_quotient_map x))
+    : forall x, P x.
+  Proof.
+    srapply Quotient_ind_hprop.
+    exact H1.
+  Defined.
+
 End QuotientGroup.
 
+Arguments QuotientGroup G N : simpl never.
 Arguments grp_quotient_map {_ _}.
 
 Notation "G / N" := (QuotientGroup G N) : group_scope.
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index a1995745f0e..d693595a7ee 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -453,6 +453,14 @@ Proof.
   exact (sgt_op sgt_unit p).
 Defined.
 
+Definition sgt_inv' {G : Group} {X} {g : G}
+  : subgroup_generated_type X (- g) -> subgroup_generated_type X g.
+Proof.
+  intros p.
+  rewrite <- grp_inv_inv.
+  by apply sgt_inv.
+Defined.
+
 Definition sgt_op' {G : Group} {X} {g h : G}
   : subgroup_generated_type X g
     -> subgroup_generated_type X h
diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index f658b7db203..c0f3b0150d7 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -209,6 +209,8 @@ Notation "x .2" := (pr2 x) : fibration_scope.
 
 Definition uncurry {A B C} (f : A -> B -> C) (p : A * B) : C := f (fst p) (snd p).
 
+Arguments uncurry {A B C} f%_function_scope p /. 
+
 (** Composition of functions. *)
 
 Notation compose := (fun g f x => g (f x)).
diff --git a/theories/Classes/theory/premetric.v b/theories/Classes/theory/premetric.v
index 06ec0fccf93..4674d0976cc 100644
--- a/theories/Classes/theory/premetric.v
+++ b/theories/Classes/theory/premetric.v
@@ -21,7 +21,6 @@ Generalizable Variables A B.
 
 Local Set Universe Minimization ToSet.
 
-
 Class Closeness@{i} (A : Type@{i}) := close : Q+ -> Relation@{i i} A.
 
 Global Instance Q_close@{} : Closeness Q := fun e q r => - ' e < q - r < ' e.
@@ -299,8 +298,7 @@ Class Continuous@{UA UB}
 Arguments continuous {A _ B _} f {_} _ _.
 
 Definition BinaryDup@{i} {A : Type@{i} } : A -> A /\ A := fun x => (x, x).
-Definition uncurry {A B C} (f : A -> B -> C) : A /\ B -> C
-  := fun x => f (fst x) (snd x).
+
 Definition map2 {A B C D} (f : A -> C) (g : B -> D) : A /\ B -> C /\ D
   := fun x => (f (fst x), g (snd x)).
 
@@ -464,7 +462,7 @@ Global Instance uncurry_lipschitz (f : A -> B -> C) L1 L2
   : Lipschitz (uncurry f) (L1 + L2).
 Proof.
 intros e [u1 u2] [v1 v2] [xi1 xi2]. simpl in xi1,xi2.
-unfold uncurry;simpl.
+simpl.
 assert (Hrw : (L1 + L2) * e = L1 * e + L2 * e)
 by abstract (apply pos_eq;ring_tac.ring_with_nat);
 rewrite Hrw;clear Hrw.
diff --git a/theories/Spaces/List/Theory.v b/theories/Spaces/List/Theory.v
index 5c18da7f420..71251638e7f 100644
--- a/theories/Spaces/List/Theory.v
+++ b/theories/Spaces/List/Theory.v
@@ -145,6 +145,15 @@ Proof.
     exact (y'; (p, inr i')).
 Defined.
 
+(** Mapping a function over a concatenated list is the concatenation of the mapped lists. *)
+Definition list_map_app {A B : Type} (f : A -> B) (l l' : list A)
+  : list_map f (l ++ l') = list_map f l ++ list_map f l'.
+Proof.
+  induction l as [|a l IHl].
+  1: reflexivity.
+  simpl; f_ap.
+Defined.
+
 (** A function that acts as the identity on the elements of a list is the identity on the mapped list. *)
 Lemma list_map_id {A : Type} (f : A -> A) (l : list A)
   (Hf : forall x, InList x l -> f x = x)
@@ -287,6 +296,33 @@ Proof.
   cbn; apply reverse_acc_cons.
 Defined.
 
+(** The [reverse] of a concatenated list is the concatenation of the reversed lists in reverse order. *)
+Definition reverse_app {A : Type} (l l' : list A)
+  : reverse (l ++ l') = reverse l' ++ reverse l.
+Proof.
+  induction l as [|a l IHl] in l' |- *.
+  1: symmetry; apply app_nil.
+  simpl.
+  lhs nrapply reverse_cons.
+  rhs nrapply ap.
+  2: nrapply reverse_cons.
+  rhs nrapply app_assoc.
+  nrapply (ap (fun l => l ++ [a])).
+  exact (IHl l').
+Defined.
+
+(** [reverse] is involutive. *)
+Definition reverse_reverse {A : Type} (l : list A)
+  : reverse (reverse l) = l.
+Proof.
+  induction l.
+  1: reflexivity.
+  lhs nrapply ap.
+  1: nrapply reverse_cons.
+  lhs nrapply reverse_app.
+  exact (ap _ IHl).
+Defined.
+
 (** ** Getting elements *)
 
 (** A variant of [nth] that returns an element of the list and a proof that it is the [n]-th element. *)
diff --git a/theories/Types/Forall.v b/theories/Types/Forall.v
index e0dd105f7e6..1aff29ca05d 100644
--- a/theories/Types/Forall.v
+++ b/theories/Types/Forall.v
@@ -366,6 +366,8 @@ Definition flip `{P : A -> B -> Type}
   : (forall a b, P a b) -> (forall b a, P a b)
   := fun f b a => f a b.
 
+Arguments flip {A B P} f b a /.
+
 Global Instance isequiv_flip `{P : A -> B -> Type}
   : IsEquiv (@flip _ _ P) | 0.
 Proof.