2 files changed, 28 insertions, 14 deletions

diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda
index 790c73a..c975d18 100644
--- a/Category/BinaryBiproducts.agda
+++ b/Category/BinaryBiproducts.agda
@@ -224,6 +224,13 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where
       [ id , ∇ ] ∘ +-assocˡ   ≈⟨ pushˡ (Equiv.sym ∇∘+₁) ⟩
       ∇ ∘ id +₁ ∇ ∘ +-assocˡ  ∎
 
+  ∇-assoc-×₁ : {A : Obj} → ∇ {A} ∘ ∇ ×₁ id ≈ ∇ ∘ id ×₁ ∇ ∘ assocˡ
+  ∇-assoc-×₁ = begin
+      ∇ ∘ ∇ ×₁ id             ≈⟨ refl⟩∘⟨ ×₁-+₁ ∇ id ⟩
+      ∇ ∘ ∇ +₁ id             ≈⟨ ∇-assoc ⟩
+      ∇ ∘ id +₁ ∇ ∘ +-assocˡ  ≈⟨ refl⟩∘⟨ ×₁-+₁ id ∇ ⟩∘⟨ assocˡ≈+-assocˡ ⟨
+      ∇ ∘ id ×₁ ∇ ∘ assocˡ    ∎
+
   Δ-assoc : {A : Obj} → id ×₁ Δ ∘ Δ {A} ≈ assocˡ ∘ Δ ×₁ id ∘ Δ
   Δ-assoc = begin
       id ×₁ Δ ∘ Δ           ≈⟨ ×₁∘Δ ⟩
@@ -262,3 +269,15 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where
       Δ ∘ f       ≈⟨ Δ∘ ⟩
       ⟨ f , f ⟩   ≈⟨ ×₁∘Δ ⟨
       f ×₁ f ∘ Δ  ∎
+
+  ⇒∇-×₁ : {A B : Obj} {f : A ⇒ B} → f ∘ ∇ ≈ ∇ ∘ f ×₁ f
+  ⇒∇-×₁ {f = f} = begin
+      f ∘ ∇       ≈⟨ ⇒∇ ⟩
+      ∇ ∘ f +₁ f  ≈⟨ refl⟩∘⟨ ×₁-+₁ f f ⟨
+      ∇ ∘ f ×₁ f  ∎
+
+  ×₁∘first : {A B C D E : Obj} {f : B ⇒ C} {g : D ⇒ E} {h : A ⇒ B} → (f ×₁ g) ∘ first h ≈ (f ∘ h) ×₁ g
+  ×₁∘first = ×₁∘×₁ ○ ×₁-cong₂ Equiv.refl identityʳ
+
+  ×₁∘second : {A B C D E : Obj} {f : A ⇒ B} {g : D ⇒ E} {h : C ⇒ D} → (f ×₁ g) ∘ second h ≈ f ×₁ (g ∘ h)
+  ×₁∘second = ×₁∘×₁ ○ ×₁-cong₂ identityʳ Equiv.refl
diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda
index 3e8dbc4..9bbc9c7 100644
--- a/Category/Semiadditive.agda
+++ b/Category/Semiadditive.agda
@@ -57,18 +57,14 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
 
     +-assoc : (x y z : A ⇒ B) → (x + y) + z ≈ x + (y + z)
     +-assoc x y z = begin
-        ∇ ∘ (∇ ∘ x ×₁ y ∘ Δ) ×₁ z ∘ Δ                           ≈⟨ refl⟩∘⟨ pushˡ (Equiv.sym first∘×₁) ⟩
-        ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y ∘ Δ) ×₁ z ∘ Δ                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-cong₂ Equiv.refl identityʳ ⟩∘⟨refl ⟨
-        ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y ∘ Δ) ×₁ (z ∘ id) ∘ Δ              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym ×₁∘×₁) ⟩
-        ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ               ≈⟨ refl⟩∘⟨ ×₁-+₁ ∇ id ⟩∘⟨refl ⟩
-        ∇ ∘ ∇ +₁ id ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ               ≈⟨ extendʳ ∇-assoc ⟩
-        ∇ ∘ (id +₁ ∇ ∘ +-assocˡ) ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ  ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ assocˡ≈+-assocˡ) ⟩∘⟨refl ⟨
-        ∇ ∘ (id +₁ ∇ ∘ assocˡ) ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ    ≈⟨ refl⟩∘⟨ pullʳ (extendʳ assocˡ∘×₁) ⟩
-        ∇ ∘ id +₁ ∇ ∘ x ×₁ (y ×₁ z) ∘ assocˡ ∘ Δ ×₁ id ∘ Δ      ≈⟨ refl⟩∘⟨ ×₁-+₁ id ∇ ⟩∘⟨ refl⟩∘⟨ Δ-assoc ⟨
-        ∇ ∘ id ×₁ ∇ ∘ x ×₁ (y ×₁ z) ∘ id ×₁ Δ ∘ Δ               ≈⟨ refl⟩∘⟨ pullˡ second∘×₁ ⟩
-        ∇ ∘ x ×₁ (∇ ∘ y ×₁ z) ∘ id ×₁ Δ ∘ Δ                     ≈⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩
-        ∇ ∘ (x ∘ id) ×₁ ((∇ ∘ y ×₁ z) ∘ Δ) ∘ Δ                  ≈⟨ refl⟩∘⟨ ×₁-cong₂ identityʳ assoc ⟩∘⟨refl ⟩
-        ∇ ∘ x ×₁ (∇ ∘ y ×₁ z ∘ Δ) ∘ Δ                           ∎
+        ∇ ∘ (∇ ∘ x ×₁ y ∘ Δ) ×₁ z ∘ Δ                         ≈⟨ refl⟩∘⟨ pushˡ (Equiv.sym first∘×₁) ⟩
+        ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y ∘ Δ) ×₁ z ∘ Δ                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym ×₁∘first) ⟩
+        ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ             ≈⟨ extendʳ ∇-assoc-×₁  ⟩
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ  ≈⟨ refl⟩∘⟨ pullʳ (extendʳ assocˡ∘×₁) ⟩
+        ∇ ∘ id ×₁ ∇ ∘ x ×₁ y ×₁ z ∘ assocˡ ∘ Δ ×₁ id ∘ Δ      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-assoc ⟨
+        ∇ ∘ id ×₁ ∇ ∘ x ×₁ y ×₁ z ∘ id ×₁ Δ ∘ Δ               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ×₁∘second ⟩
+        ∇ ∘ id ×₁ ∇ ∘ x ×₁ (y ×₁ z ∘ Δ) ∘ Δ                   ≈⟨ refl⟩∘⟨ pullˡ second∘×₁ ⟩
+        ∇ ∘ x ×₁ (∇ ∘ y ×₁ z ∘ Δ) ∘ Δ                         ∎
 
     +-identityˡ : (x : A ⇒ B) → zero⇒ + x ≈ x
     +-identityˡ x = begin
@@ -141,8 +137,7 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
         {k : C ⇒ D}
       → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h
   +-resp-∘ {f = f} {g} {h} {k} = begin
-      k ∘ (∇ ∘ f ×₁ g ∘ Δ) ∘ h            ≈⟨ extendʳ (extendʳ ⇒∇) ⟩
-      ∇ ∘ (k +₁ k ∘ f ×₁ g ∘ Δ) ∘ h       ≈⟨ refl⟩∘⟨ (×₁-+₁ k k ⟩∘⟨refl) ⟩∘⟨refl ⟨
+      k ∘ (∇ ∘ f ×₁ g ∘ Δ) ∘ h            ≈⟨ extendʳ (extendʳ ⇒∇-×₁) ⟩
       ∇ ∘ (k ×₁ k ∘ f ×₁ g ∘ Δ) ∘ h       ≈⟨ refl⟩∘⟨ pullʳ (pullʳ ⇒Δ) ⟩
       ∇ ∘ k ×₁ k ∘ f ×₁ g ∘ h ×₁ h ∘ Δ    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩
       ∇ ∘ k ×₁ k ∘ (f ∘ h) ×₁ (g ∘ h) ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩