Add hom-set addition to semiadditive recordmain

7 files changed, 283 insertions, 117 deletions

diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda
index 3ded5a7..bc0fac8 100644
--- a/Category/BinaryBiproducts.agda
+++ b/Category/BinaryBiproducts.agda
@@ -329,3 +329,15 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where
       ⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩
       ⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩   ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩
       ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩                                                       ∎
+
+  σ₂₃-⟨⟩-×₁
+      : {X Y A B : Obj}
+        {f : X ⇒ A}
+        {g : Y ⇒ B}
+        {h : X ⇒ A}
+        {i : Y ⇒ B}
+      → σ₂₃ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈ ⟨ f , h ⟩ ×₁ ⟨ g , i ⟩
+  σ₂₃-⟨⟩-×₁ {f = f} {g} {h} {i} = begin
+      σ₂₃ ∘ ⟨ f ×₁ g , h ×₁ i ⟩                     ≈⟨ σ₂₃-⟨⟩ ⟩
+      ⟨ ⟨ f ∘ π₁ , h ∘ π₁ ⟩ , ⟨ g ∘ π₂ , i ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ⟨⟩∘ ⟨⟩∘ ⟨
+      ⟨ ⟨ f , h ⟩ ∘ π₁ , ⟨ g , i ⟩ ∘ π₂ ⟩           ∎
diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda
index 41be19e..8c46e14 100644
--- a/Category/Dagger/Semiadditive.agda
+++ b/Category/Dagger/Semiadditive.agda
@@ -106,10 +106,14 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
 
   +-† : {A B : Obj} {f g : A ⇒ B} → (f + g) † ≈ (f †) + (g †)
   +-† {f = f} {g} = begin
-      (∇ ∘ f ×₁ g ∘ Δ) †     ≈⟨ †-homomorphism ⟩
-      (f ×₁ g ∘ Δ) † ∘ ∇ †   ≈⟨ pushˡ †-homomorphism ⟩
-      Δ † ∘ (f ×₁ g) † ∘ ∇ † ≈⟨ Δ† ⟩∘⟨ †-resp-×₁ ⟩∘⟨ ∇† ⟩
-      ∇ ∘ (f †) ×₁ (g †) ∘ Δ ∎
+      (f + g) †               ≈⟨ ⟨ +-∇∘⟨⟩ ⟩† ⟩
+      (∇ ∘ ⟨ f , g ⟩) †       ≈⟨ †-homomorphism ⟩
+      ⟨ f , g ⟩ † ∘ ∇ †       ≈⟨ refl⟩∘⟨ ∇† ⟩
+      ⟨ f , g ⟩ † ∘ Δ         ≈⟨ ⟨⟩-† ⟩∘⟨refl ⟩
+      [ f † , g † ] ∘ Δ       ≈⟨ pushˡ (Equiv.sym ∇∘×₁) ⟩
+      ∇ ∘ (f †) ×₁ (g †) ∘ Δ  ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩
+      ∇ ∘ ⟨ f † , g † ⟩       ≈⟨ +-∇∘⟨⟩ ⟨
+      (f †) + (g †)           ∎
 
   -- bilinearity of composition
   ∘-distribˡ : {A B C : Obj} {f : B ⇒ C} {g h : A ⇒ B} → f ∘ (g + h) ≈ f ∘ g + f ∘ h
@@ -170,9 +174,9 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
 
   ≤-trans : {A B : Obj} {f g h : A ⇒ B} → f ≤ g → g ≤ h → f ≤ h
   ≤-trans {A} {B} {f} {g} {h} f≤g g≤h = begin
-      f + h       ≈⟨ refl⟩∘⟨ ×₁-congˡ g≤h ⟩∘⟨refl ⟨
+      f + h       ≈⟨ +-congˡ g≤h ⟨
       f + (g + h) ≈⟨ +-assoc f g h ⟨
-      (f + g) + h ≈⟨ refl⟩∘⟨ ×₁-congʳ f≤g ⟩∘⟨refl ⟩
+      (f + g) + h ≈⟨ +-congʳ f≤g ⟩
       g + h       ≈⟨ g≤h ⟩
       h           ∎
 
@@ -199,14 +203,13 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       → g ≤ i
       → (f ×₁ g) ≤ (h ×₁ i)
   ≤-resp-×₁ {f = f} {h} {g} {i} f≤h g≤i = begin
-      ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ Δ                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-⊕ ⟩
-      ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ∘ Δ ×₁ Δ             ≈⟨ refl⟩∘⟨ extendʳ σ₂₃-×₁ ⟩
-      ∇ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ             ≈⟨ pushˡ ∇-⊕ ⟩
-      ∇ ×₁ ∇ ∘ σ₂₃ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ  ≈⟨ refl⟩∘⟨ cancelˡ σ₂₃-σ₂₃ ⟩
-      ∇ ×₁ ∇ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ              ≈⟨ refl⟩∘⟨ ×₁∘×₁ ⟩
-      ∇ ×₁ ∇ ∘ (f ×₁ h ∘ Δ) ×₁ (g ×₁ i ∘ Δ)               ≈⟨ ×₁∘×₁ ⟩
-      (∇ ∘ f ×₁ h ∘ Δ) ×₁ (∇ ∘ g ×₁ i ∘ Δ)                ≈⟨ ×₁-cong₂ f≤h g≤i ⟩
-      h ×₁ i                                              ∎
+      f ×₁ g + h ×₁ i                    ≈⟨ +-∇∘⟨⟩ ⟩
+      ∇ ∘ ⟨ f ×₁ g , h ×₁ i ⟩            ≈⟨ pushˡ ∇-⊕ ⟩
+      ∇ ×₁ ∇ ∘ σ₂₃ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈⟨ refl⟩∘⟨ σ₂₃-⟨⟩-×₁ ⟩
+      ∇ ×₁ ∇ ∘ ⟨ f , h ⟩ ×₁ ⟨ g , i ⟩    ≈⟨ ×₁∘×₁ ⟩
+      (∇ ∘ ⟨ f , h ⟩) ×₁ (∇ ∘ ⟨ g , i ⟩) ≈⟨ ×₁-cong₂ +-∇∘⟨⟩ +-∇∘⟨⟩ ⟨
+      (f + h) ×₁ (g + i)                 ≈⟨ ×₁-cong₂ f≤h g≤i ⟩
+      h ×₁ i                            ∎
 
   ≤-resp-∘
       : {A B C : Obj}
@@ -234,9 +237,9 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
   -- special law
   ∇∘Δ : {A : Obj} → ∇ ∘ Δ ≈ id {A}
   ∇∘Δ = begin
-      ∇ ∘ Δ             ≈⟨ refl⟩∘⟨ introˡ id×₁id ⟩
-      ∇ ∘ id ×₁ id ∘ Δ  ≈⟨ idempotent ⟩
-      id                ∎
+      ∇ ∘ Δ   ≈⟨ +-∇∘⟨⟩ ⟨
+      id + id ≈⟨ idempotent ⟩
+      id      ∎
 
   dagger-2-poset : Dagger-2-Poset
   dagger-2-poset = record
diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda
index 7d34fbf..30f84e6 100644
--- a/Category/Semiadditive.agda
+++ b/Category/Semiadditive.agda
@@ -18,7 +18,10 @@ open import Categories.Object.Zero 𝒞 using (Zero)
 open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts)
 open import Data.Product using (_,_)
 
-private module 𝒞 = Category 𝒞
+private
+  module 𝒞 = Category 𝒞
+  variable
+    A B C D : 𝒞.Obj
 
 -- A semiadditive category has all finite biproducts
 record Semiadditive : Set (levelOfTerm 𝒞) where
@@ -32,9 +35,43 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
 
   open 𝒞
 
+  infix 8 _+_
+
+  field
+    𝟎 : A ⇒ B
+    𝟎-resp-∘ : {h : A ⇒ B} {k : C ⇒ D} → k ∘ 𝟎 ∘ h ≈ 𝟎
+    _+_ : A ⇒ B → A ⇒ B → A ⇒ B
+    +-resp-≈ : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v
+    +-resp-∘ : {f g : B ⇒ C} {h : A ⇒ B} {k : C ⇒ D} → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h
+    +-identityˡ : (f : A ⇒ B) → 𝟎 + f ≈ f
+    +-identityʳ : (f : A ⇒ B) → f + 𝟎 ≈ f
+
   open HomReasoning
   open ⇒-Reasoning
 
+  +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v
+  +-cong = +-resp-≈
+
+  +-resp-∘ˡ
+      : {A B C : Obj}
+        {f g : A ⇒ B}
+        {k : B ⇒ C}
+      → k ∘ (f + g) ≈ k ∘ f + k ∘ g
+  +-resp-∘ˡ {f = f} {g} {h} = begin
+      h ∘ (f + g)             ≈⟨ refl⟩∘⟨ identityʳ ⟨
+      h ∘ (f + g) ∘ id        ≈⟨ +-resp-∘ ⟩
+      h ∘ f ∘ id + h ∘ g ∘ id ≈⟨ +-resp-≈ (refl⟩∘⟨ identityʳ) (refl⟩∘⟨ identityʳ) ⟩
+      h ∘ f + h ∘ g           ∎
+
+  𝟎-resp-∘ˡ
+      : {A B C : Obj}
+        {f : B ⇒ C}
+      → f ∘ 𝟎 {A} {B} ≈ 𝟎
+  𝟎-resp-∘ˡ {f = f} = begin
+      f ∘ 𝟎       ≈⟨ refl⟩∘⟨ identityʳ ⟨
+      f ∘ 𝟎 ∘ id  ≈⟨ 𝟎-resp-∘ ⟩
+      𝟎           ∎
+
   module _ {A B : Obj} where
 
     π₁∘i₂≈0 : π₁ {A} {B} ∘ i₂ ≈ zero⇒
@@ -49,6 +86,38 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
         zero⇒ {A} ∘ π₂ ∘ i₁ ≈⟨ zero-∘ʳ (π₂ ∘ i₁) ⟩
         zero⇒               ∎
 
+    𝟎≈zero⇒ : 𝟎 {A} {B} ≈ zero⇒
+    𝟎≈zero⇒ = begin
+        𝟎         ≈⟨ 𝟎-resp-∘ˡ ⟨
+        zero⇒ ∘ 𝟎 ≈⟨ zero-∘ʳ {A} {B} 𝟎 ⟩
+        zero⇒     ∎
+
+  module _ {A B : Obj} where
+
+    +-∇∘⟨⟩ : {f g : A ⇒ B} → f + g ≈ ∇ ∘ ⟨ f , g ⟩
+    +-∇∘⟨⟩ {f} {g} = begin
+        f + g                   ≈⟨ +-resp-≈ (insertˡ inject₁) (insertˡ inject₂) ⟩
+        ∇ ∘ i₁ ∘ f + ∇ ∘ i₂ ∘ g ≈⟨ +-resp-∘ˡ ⟨
+        ∇ ∘ (i₁ ∘ f + i₂ ∘ g)   ≈⟨ refl⟩∘⟨ ⟨⟩-unique left right ⟨
+        ∇ ∘ ⟨ f , g ⟩           ∎
+      where
+        left : π₁ ∘ (i₁ ∘ f + i₂ ∘ g) ≈ f
+        left = begin
+            π₁ ∘ (i₁ ∘ f + i₂ ∘ g)    ≈⟨ +-resp-∘ˡ ⟩
+            π₁ ∘ i₁ ∘ f + π₁ ∘ i₂ ∘ g ≈⟨ +-resp-≈ (cancelˡ π₁∘i₁≈id) (pullˡ π₁∘i₂≈0) ⟩
+            f + zero⇒ ∘ g             ≈⟨ +-resp-≈ Equiv.refl (zero-∘ʳ g) ⟩
+            f + zero⇒                 ≈⟨ +-resp-≈ Equiv.refl 𝟎≈zero⇒ ⟨
+            f + 𝟎                     ≈⟨ +-identityʳ f ⟩
+            f                         ∎
+        right : π₂ ∘ (i₁ ∘ f + i₂ ∘ g) ≈ g
+        right = begin
+            π₂ ∘ (i₁ ∘ f + i₂ ∘ g)    ≈⟨ +-resp-∘ˡ ⟩
+            π₂ ∘ i₁ ∘ f + π₂ ∘ i₂ ∘ g ≈⟨ +-resp-≈ (pullˡ π₂∘i₁≈0) (cancelˡ π₂∘i₂≈id) ⟩
+            zero⇒ ∘ f + g             ≈⟨ +-resp-≈ (zero-∘ʳ f) Equiv.refl ⟩
+            zero⇒ + g                 ≈⟨ +-resp-≈ 𝟎≈zero⇒ Equiv.refl ⟨
+            𝟎 + g                     ≈⟨ +-identityˡ g ⟩
+            g                         ∎
+
   Δ-⊕ : {X Y : Obj} → Δ {X ⊕ Y} ≈ σ₂₃ ∘ Δ ×₁ Δ
   Δ-⊕ {X} {Y} = begin
       ⟨ id , id ⟩                                     ≈⟨ ⟨⟩-cong₂ id×₁id id×₁id ⟨
@@ -69,45 +138,17 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
 
   module _ {A B : Obj} where
 
-    _+_ _+′_ : A ⇒ B → A ⇒ B → A ⇒ B
-    f + g = ∇ ∘ f ×₁ g ∘ Δ
-    f +′ g = ∇ ∘ f +₁ g ∘ Δ
-
-    infix 8 _+_
-
-    +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v
-    +-cong eq₁ eq₂ = refl⟩∘⟨ ×₁-cong₂ eq₁ eq₂ ⟩∘⟨refl
-
     +-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⟩∘⟨ 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
-        ∇ ∘ zero⇒ ×₁ x ∘ Δ              ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩
-        ∇ ∘ ⟨ zero⇒ , x ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (zero-∘ʳ x) identityˡ ⟨
-        ∇ ∘ ⟨ zero⇒ ∘ x , id ∘ x ⟩      ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨
-        ∇ ∘ ⟨ zero⇒ , id ⟩ ∘ x          ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₂≈0 π₂∘i₂≈id ⟩∘⟨refl ⟨
-        ∇ ∘ ⟨ π₁ ∘ i₂ , π₂ ∘ i₂ ⟩ ∘ x   ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩
-        ∇ ∘ i₂ ∘ x                      ≈⟨ cancelˡ ∇-identityˡ ⟩
-        x                               ∎
-
-    +-identityʳ : (x : A ⇒ B) → x + zero⇒ ≈ x
-    +-identityʳ x = begin
-        ∇ ∘ x ×₁ zero⇒ ∘ Δ              ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩
-        ∇ ∘ ⟨ x , zero⇒ ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ (zero-∘ʳ x) ⟨
-        ∇ ∘ ⟨ id ∘ x , zero⇒ ∘ x ⟩      ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨
-        ∇ ∘ ⟨ id , zero⇒ ⟩ ∘ x          ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₁≈id π₂∘i₁≈0 ⟩∘⟨refl ⟨
-        ∇ ∘ ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ∘ x   ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩
-        ∇ ∘ i₁ ∘ x                      ≈⟨ cancelˡ ∇-identityʳ ⟩
-        x                               ∎
+        (x + y) + z                                 ≈⟨ +-∇∘⟨⟩ ⟩
+        ∇ ∘ ⟨ x + y , z ⟩                           ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ +-∇∘⟨⟩ ⟩
+        ∇ ∘ ⟨ ∇ ∘ ⟨ x , y ⟩ , z ⟩                   ≈⟨ refl⟩∘⟨ first∘⟨⟩ ⟨
+        ∇ ∘ ∇ ×₁ id ∘ ⟨ ⟨ x , y ⟩ , z ⟩             ≈⟨ extendʳ ∇-assoc-×₁ ⟩
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ x , y ⟩ , z ⟩  ≈⟨ refl⟩∘⟨ pullʳ assocˡ∘⟨⟩ ⟩
+        ∇ ∘ id ×₁ ∇ ∘ ⟨ x , ⟨ y , z ⟩ ⟩             ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟩
+        ∇ ∘ ⟨ x , ∇ ∘ ⟨ y , z ⟩ ⟩                   ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ +-∇∘⟨⟩ ⟨
+        ∇ ∘ ⟨ x , y + z ⟩                           ≈⟨ +-∇∘⟨⟩ ⟨
+        x + (y + z)                                 ∎
 
     ∇∘+-swap : {A : Obj} → ∇ ∘ +-swap {A} ≈ ∇
     ∇∘+-swap = begin
@@ -123,19 +164,20 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
 
     +-comm : (x y : A ⇒ B) → x + y ≈ y + x
     +-comm x y = begin
-        ∇ ∘ x ×₁ y ∘ Δ          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘Δ ⟨
-        ∇ ∘ x ×₁ y ∘ swap ∘ Δ   ≈⟨ refl⟩∘⟨ extendʳ swap∘×₁ ⟨
-        ∇ ∘ swap ∘ y ×₁ x ∘ Δ   ≈⟨ refl⟩∘⟨ swap≈+-swap ⟩∘⟨refl ⟩
-        ∇ ∘ +-swap ∘ y ×₁ x ∘ Δ ≈⟨ pullˡ ∇∘+-swap ⟩
-        ∇ ∘ y ×₁ x ∘ Δ          ∎
-
-    isCM : IsCommutativeMonoid (_≈_ {A} {B}) _+_ zero⇒
+        x + y                   ≈⟨ +-∇∘⟨⟩ ⟩
+        ∇ ∘ ⟨ x , y ⟩           ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨
+        ∇ ∘ swap ∘ ⟨ y , x ⟩    ≈⟨ refl⟩∘⟨ swap≈+-swap ⟩∘⟨refl ⟩
+        ∇ ∘ +-swap ∘ ⟨ y , x ⟩  ≈⟨ pullˡ ∇∘+-swap ⟩
+        ∇ ∘ ⟨ y , x ⟩           ≈⟨ +-∇∘⟨⟩ ⟨
+        y + x                   ∎
+
+    isCM : IsCommutativeMonoid (_≈_ {A} {B}) _+_ 𝟎
     isCM = record
         { isMonoid = record
             { isSemigroup = record
                 { isMagma = record
                     { isEquivalence = equiv
-                    ; ∙-cong = +-cong
+                    ; ∙-cong = +-resp-≈
                     }
                 ; assoc = +-assoc
                 }
@@ -149,39 +191,16 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
       { Carrier = A ⇒ B
       ; _≈_ = _≈_
       ; _∙_ = _+_
-      ; ε = zero⇒
+      ; ε = 𝟎
       ; isCommutativeMonoid = isCM
       }
 
-  +-resp-∘
-      : {A B C D : Obj}
-        {f g : B ⇒ C}
-        {h : A ⇒ B}
-        {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⟩∘⟨ pullʳ (pullʳ ⇒Δ) ⟩
-      ∇ ∘ k ×₁ k ∘ f ×₁ g ∘ h ×₁ h ∘ Δ    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩
-      ∇ ∘ k ×₁ k ∘ (f ∘ h) ×₁ (g ∘ h) ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩
-      ∇ ∘ (k ∘ f ∘ h) ×₁ (k ∘ g ∘ h) ∘ Δ  ∎
-
-  0-resp-∘
-      : {A C D : Obj}
-        {h : A ⇒ C}
-        {k : C ⇒ D}
-      → k ∘ zero⇒ ∘ h ≈ zero⇒
-  0-resp-∘ {h = h} {k} = begin
-      k ∘ zero⇒ ∘ h ≈⟨ pullˡ (zero-∘ˡ k) ⟩
-      zero⇒ ∘ h     ≈⟨ zero-∘ʳ h ⟩
-      zero⇒         ∎
-
   cm-category : CM-Category o ℓ e
   cm-category = record
       { 𝒞
       ; Hom = hom
       ; +-resp-∘ = +-resp-∘
-      ; 0-resp-∘ = 0-resp-∘
+      ; 0-resp-∘ = 𝟎-resp-∘
       }
 
   cartesian : Cartesian
@@ -195,3 +214,98 @@ record Semiadditive : Set (levelOfTerm 𝒞) where
       { initial = initial
       ; coproducts = binaryCoproducts
       }
+
+record SemiadditiveHelper : Set (levelOfTerm 𝒞) where
+
+  field
+    zero : Zero
+    biproducts : BinaryBiproducts
+
+  open Zero zero
+  open BinaryBiproducts biproducts
+  open 𝒞
+  open HomReasoning
+  open ⇒-Reasoning
+
+  module _ {A B : Obj} where
+
+    π₁∘i₂≈0 : π₁ {A} {B} ∘ i₂ ≈ zero⇒
+    π₁∘i₂≈0 = begin
+        π₁ ∘ i₂             ≈⟨ π₁i₂-absorbˡ zero⇒ ⟨
+        zero⇒ {A} ∘ π₁ ∘ i₂ ≈⟨ zero-∘ʳ (π₁ ∘ i₂) ⟩
+        zero⇒               ∎
+
+    π₂∘i₁≈0 : π₂ {A} {B} ∘ i₁ ≈ zero⇒
+    π₂∘i₁≈0 = begin
+        π₂ ∘ i₁             ≈⟨ π₂i₁-absorbˡ zero⇒ ⟨
+        zero⇒ {A} ∘ π₂ ∘ i₁ ≈⟨ zero-∘ʳ (π₂ ∘ i₁) ⟩
+        zero⇒               ∎
+
+-- Construct hom-set addition from biproduct
+semiadditveHelper : SemiadditiveHelper → Semiadditive
+semiadditveHelper sh = record
+    { zero = zero
+    ; biproducts = biproducts
+    ; 𝟎 = zero⇒
+    ; 𝟎-resp-∘ = 𝟎-resp-∘
+    ; _+_ = _+_
+    ; +-resp-≈ = +-cong
+    ; +-resp-∘ = +-resp-∘
+    ; +-identityˡ = +-identityˡ
+    ; +-identityʳ = +-identityʳ
+    }
+  where
+    open SemiadditiveHelper sh
+    open Zero zero
+    open BinaryBiproducts biproducts
+    open 𝒞
+    open HomReasoning
+    open ⇒-Reasoning
+
+    𝟎-resp-∘
+        : {A B C D : Obj}
+          {h : A ⇒ B}
+          {k : C ⇒ D}
+        → k ∘ zero⇒ ∘ h ≈ zero⇒
+    𝟎-resp-∘ {h = h} {k} = begin
+        k ∘ zero⇒ ∘ h ≈⟨ pullˡ (zero-∘ˡ k) ⟩
+        zero⇒ ∘ h     ≈⟨ zero-∘ʳ h ⟩
+        zero⇒         ∎
+
+    infix 8 _+_
+
+    _+_ : A ⇒ B → A ⇒ B → A ⇒ B
+    f + g = ∇ ∘ ⟨ f , g ⟩
+
+    +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v
+    +-cong eq₁ eq₂ = refl⟩∘⟨ ⟨⟩-cong₂ eq₁ eq₂
+
+    +-resp-∘
+        : {A B C D : Obj}
+          {f g : B ⇒ C}
+          {h : A ⇒ B}
+          {k : C ⇒ D}
+        → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h
+    +-resp-∘ {f = f} {g} {h} {k} = begin
+        k ∘ (∇ ∘ ⟨ f , g ⟩) ∘ h         ≈⟨ refl⟩∘⟨ pullʳ ⟨⟩∘ ⟩
+        k ∘ ∇ ∘ ⟨ f ∘ h , g ∘ h ⟩       ≈⟨ extendʳ ⇒∇-×₁ ⟩
+        ∇ ∘ k ×₁ k ∘ ⟨ f ∘ h , g ∘ h ⟩  ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩
+        ∇ ∘ ⟨ k ∘ f ∘ h , k ∘ g ∘ h ⟩   ∎
+
+    +-identityˡ : (x : A ⇒ B) → zero⇒ + x ≈ x
+    +-identityˡ x = begin
+        ∇ ∘ ⟨ zero⇒ , x ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (zero-∘ʳ x) identityˡ ⟨
+        ∇ ∘ ⟨ zero⇒ ∘ x , id ∘ x ⟩      ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨
+        ∇ ∘ ⟨ zero⇒ , id ⟩ ∘ x          ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₂≈0 π₂∘i₂≈id ⟩∘⟨refl ⟨
+        ∇ ∘ ⟨ π₁ ∘ i₂ , π₂ ∘ i₂ ⟩ ∘ x   ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩
+        ∇ ∘ i₂ ∘ x                      ≈⟨ cancelˡ ∇-identityˡ ⟩
+        x                               ∎
+
+    +-identityʳ : (x : A ⇒ B) → x + zero⇒ ≈ x
+    +-identityʳ x = begin
+        ∇ ∘ ⟨ x , zero⇒ ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ (zero-∘ʳ x) ⟨
+        ∇ ∘ ⟨ id ∘ x , zero⇒ ∘ x ⟩      ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨
+        ∇ ∘ ⟨ id , zero⇒ ⟩ ∘ x          ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₁≈id π₂∘i₁≈0 ⟩∘⟨refl ⟨
+        ∇ ∘ ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ∘ x   ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩
+        ∇ ∘ i₁ ∘ x                      ≈⟨ cancelˡ ∇-identityʳ ⟩
+        x                               ∎
diff --git a/Data/Matrix/Category.agda b/Data/Matrix/Category.agda
index 717926a..e1a10ec 100644
--- a/Data/Matrix/Category.agda
+++ b/Data/Matrix/Category.agda
@@ -13,8 +13,8 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Categories.Category using (Category)
 open import Categories.Category.Helper using (categoryHelper)
 open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _ᵀᵀ; _∥_; _≑_; mapₕ; mapᵥ; ∷ᵥⁿ; ∷ₕⁿ; columns-∷ₕⁿ; ∷ᵥⁿ-ᵀ)
-open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; ᵀ-cong; module ≋)
-open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_)
+open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; ᵀ-cong; module ≋; ∥-cong; ≑-cong)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong)
 open import Data.Matrix.Transform R using ([_]_; _[_]; -[-]-cong; [-]--cong; -[-]ᵀ; []-∙; [-]--∥; [++]-≑; I; Iᵀ; I[-]; map--[-]-I; [-]-𝟎; [⟨0⟩]-)
 open import Data.Nat using (ℕ)
 open import Data.Vec using (Vec; map)
@@ -176,6 +176,36 @@ opaque
   ·-𝟎ˡ {A} {B} {zero} M = PW.[]
   ·-𝟎ˡ {A} {B} {suc C} M = [⟨0⟩]- M PW.∷ ·-𝟎ˡ M
 
+·-[+]ˡ
+    : (W : Matrix B C)
+      (Y Z : Matrix A B)
+    → W · (Y [+] Z) ≋ (W · Y) [+] (W · Z)
+·-[+]ˡ {C = C} {A = A} W Y Z = begin
+    W · (Y [+] Z)               ≈⟨ ·-resp-≋ ≋.refl ([+]-cong ·-Iˡ ·-Iˡ) ⟨
+    W · ((I · Y) [+] (I · Z))   ≈⟨ ·-resp-≋ ≋.refl (∥-·-≑ I I Y Z) ⟨
+    W · (I ∥ I) · (Y ≑ Z)       ≈⟨ ·-assoc ⟨
+    (W · (I ∥ I)) · (Y ≑ Z)     ≡⟨ ≡.cong (_· (Y ≑ Z)) (·-∥ W I I) ⟩
+    (W · I ∥ W · I) · (Y ≑ Z)   ≈⟨ ·-resp-≋ (∥-cong ·-Iʳ ·-Iʳ) ≋.refl ⟩
+    (W ∥ W) · (Y ≑ Z)           ≈⟨ ∥-·-≑ W W Y Z ⟩
+    (W · Y) [+] (W · Z)         ∎
+  where
+    open ≈-Reasoning (Matrixₛ A C)
+
+·-[+]ʳ
+    : (W : Matrix A B)
+      (Y Z : Matrix B C)
+    → (Y [+] Z) · W ≋ (Y · W) [+] (Z · W)
+·-[+]ʳ {A = A} {C = C} W Y Z = begin
+    (Y [+] Z) · W                 ≈⟨ ·-resp-≋ ([+]-cong ·-Iʳ ·-Iʳ) ≋.refl ⟨
+    ((Y · I) [+] (Z · I)) · W     ≈⟨ ·-resp-≋ (∥-·-≑ Y Z I I) ≋.refl ⟨
+    ((Y ∥ Z) · (I ≑ I)) · W       ≈⟨ ·-assoc ⟩
+    (Y ∥ Z) · ((I ≑ I) · W)       ≡⟨ ≡.cong ((Y ∥ Z) ·_) (≑-· I I W) ⟩
+    (Y ∥ Z) · ((I · W) ≑ (I · W)) ≈⟨ ·-resp-≋ ≋.refl (≑-cong ·-Iˡ ·-Iˡ) ⟩
+    (Y ∥ Z) · (W ≑ W)             ≈⟨ ∥-·-≑ Y Z W W ⟩
+    (Y · W) [+] (Z · W)           ∎
+  where
+    open ≈-Reasoning (Matrixₛ A C)
+
 -- The category of matrices over a rig
 Mat : Category 0ℓ c (c ⊔ ℓ)
 Mat = categoryHelper record
diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda
index 1b7b07f..319b4f9 100644
--- a/Data/Matrix/Dagger-2-Poset.agda
+++ b/Data/Matrix/Dagger-2-Poset.agda
@@ -45,32 +45,10 @@ opaque
   [+]-idem [] = PW.[]
   [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M
 
-+-[+] : (M N : Matrix A B) → (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (N · (𝟎 ∥ I))) · (I ≑ I) ≋ M [+] N
-+-[+] M N = begin
-    (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (N · (𝟎 ∥ I))) · (I ≑ I)         ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ≑ h₂) · (I ≑ I)) (·-∥ M I 𝟎) (·-∥ N 𝟎 I) ⟩
-    (I ∥ I) · ((M · I) ∥ (M · 𝟎) ≑ (N · 𝟎) ∥ (N · I)) · (I ≑ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (≑-cong (∥-cong ·-Iʳ (·-𝟎ʳ M)) (∥-cong (·-𝟎ʳ N) ·-Iʳ)) ≋.refl) ⟩
-    (I ∥ I) · ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) · (I ≑ I)                     ≡⟨ ≡.cong ((I ∥ I) ·_) (≑-· (M ∥ 𝟎) (𝟎 ∥ N) (I ≑ I)) ⟩
-    (I ∥ I) · (((M ∥ 𝟎) · (I ≑ I)) ≑ ((𝟎 ∥ N) · (I ≑ I)))       ≈⟨ ∥-·-≑ I I ((M ∥ 𝟎) · (I ≑ I)) ((𝟎 ∥ N) · (I ≑ I)) ⟩
-    (I · (M ∥ 𝟎) · (I ≑ I)) [+] (I · (𝟎 ∥ N) · (I ≑ I))         ≈⟨ [+]-cong ·-Iˡ ·-Iˡ ⟩
-    ((M ∥ 𝟎) · (I ≑ I)) [+] ((𝟎 ∥ N) · (I ≑ I))                 ≈⟨ [+]-cong (∥-·-≑ M 𝟎 I I) (∥-·-≑ 𝟎 N I I) ⟩
-    ((M · I) [+] (𝟎 · I)) [+] ((𝟎 · I) [+] (N · I))             ≈⟨ [+]-cong ([+]-cong ·-Iʳ ·-Iʳ) ([+]-cong ·-Iʳ ·-Iʳ) ⟩
-    (M [+] 𝟎) [+] (𝟎 [+] N)                                     ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ N) ⟩
-    M [+] N                                                     ∎
-  where
-    open ≈-Reasoning (Matrixₛ _ _)
-
-idem : (M : Matrix A B) → (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≋ M
-idem M = begin
-    (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≈⟨ +-[+] M M ⟩
-    M [+] M                                             ≈⟨ [+]-idem M ⟩
-    M                                                   ∎
-  where
-    open ≈-Reasoning (Matrixₛ _ _)
-
 Mat-IdempotentSemiadditiveDagger : IdempotentSemiadditiveDagger Mat
 Mat-IdempotentSemiadditiveDagger = record
     { semiadditiveDagger = Mat-SemiadditiveDagger
-    ; idempotent = idem _
+    ; idempotent = [+]-idem _
     }
 
 open IdempotentSemiadditiveDagger Mat-IdempotentSemiadditiveDagger
diff --git a/Data/Matrix/Semiadditive.agda b/Data/Matrix/Semiadditive.agda
index babbdfa..dd24d15 100644
--- a/Data/Matrix/Semiadditive.agda
+++ b/Data/Matrix/Semiadditive.agda
@@ -21,7 +21,7 @@ open import Categories.Object.Product using (IsProduct)
 open import Categories.Object.Terminal using (IsTerminal)
 open import Categories.Object.Zero using (Zero)
 open import Category.Semiadditive using (Semiadditive)
-open import Data.Matrix.Category R using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc)
+open import Data.Matrix.Category R using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc; ·-[+]ˡ; ·-[+]ʳ)
 open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong)
 open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ)
 open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapₕ; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!)
@@ -257,12 +257,39 @@ zeroObj = record
         }
     }
 
+𝟎-resp-· : {M : Matrix C D} {N : Matrix A B} → M · 𝟎 {B} {C} · N ≋ 𝟎 {A} {D}
+𝟎-resp-· {D = D} {A = A} {M = M} {N} = begin
+    M · 𝟎 · N ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ N) ⟩
+    M · 𝟎     ≈⟨ ·-𝟎ʳ M ⟩
+    𝟎         ∎
+  where
+    open ≈-Reasoning (Matrixₛ A D)
+
+[+]-resp-·
+    : {M N : Matrix B C}
+      {H : Matrix A B}
+      {K : Matrix C D}
+    → K · (M [+] N) · H ≋ (K · M · H) [+] (K · N · H)
+[+]-resp-· {A = A} {D = D} {M = M} {N} {H} {K} = begin
+    K · (M [+] N) · H           ≈⟨ ·-resp-≋ ≋.refl (·-[+]ʳ H M N) ⟩
+    K · ((M · H) [+] (N · H))   ≈⟨ ·-[+]ˡ K (M · H) (N · H) ⟩
+    (K · M · H) [+] (K · N · H) ∎
+  where
+    open ≈-Reasoning (Matrixₛ A D)
+
 Mat-Semiadditive : Semiadditive Mat
 Mat-Semiadditive = record
     { zero = zeroObj
     ; biproducts = record
         { biproduct = biproduct
         }
+    ; 𝟎 = 𝟎
+    ; 𝟎-resp-∘ = 𝟎-resp-·
+    ; _+_ = _[+]_
+    ; +-resp-≈ = [+]-cong
+    ; +-resp-∘ = [+]-resp-·
+    ; +-identityˡ = [+]-𝟎ˡ
+    ; +-identityʳ = [+]-𝟎ʳ
     }
 
 open Semiadditive Mat-Semiadditive
diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda
index 1c3928e..a932c61 100644
--- a/Data/WiringDiagram/Equalities.agda
+++ b/Data/WiringDiagram/Equalities.agda
@@ -57,9 +57,9 @@ loop∘push∘loop≈merge f id≤f†∘f = ≈ᵢ ⌸ (identityˡ ○ identity
         ∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , (f † ∘ f) ×₁ (f †) ⟩                             ≈⟨ refl⟩∘⟨ pushʳ (sym assocˡ∘⟨⟩) ⟩
         ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ (⟨⟩-congʳ identityˡ) ⟨
         ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ id ∘ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟨
-        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †)                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-congʳ ×₁∘Δ ⟨
-        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †)               ≈⟨ extendʳ ∇-assoc-×₁ ⟨
-        ∇ ∘ (∇ ×₁ id) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †)                        ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †)                    ≈⟨ extendʳ ∇-assoc-×₁ ⟨
+        ∇ ∘ (∇ ×₁ id) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †)                             ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (∇ ∘ ⟨ id , f † ∘ f ⟩) ×₁ (f †)                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ +-∇∘⟨⟩ ⟨
         ∇ ∘ (id + (f † ∘ f)) ×₁ (f †)                                         ≈⟨ refl⟩∘⟨ ×₁-congʳ id≤f†∘f ⟩
         ∇ ∘ (f † ∘ f) ×₁ (f †)                                                ≈⟨ refl⟩∘⟨ ×₁∘first ⟨
         ∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id                                          ≈⟨ extendʳ ⇒∇-×₁ ⟨
@@ -93,6 +93,8 @@ loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identity
         ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id                   ≈⟨ extendʳ ∇-assoc-×₁ ⟨
         ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id                              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘first ⟩
         ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †) ∘ Δ) ×₁ f                                    ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (∇ ∘ id ×₁ (f ∘ f †) ∘ Δ) ×₁ f                                          ≈⟨ refl⟩∘⟨ ×₁-congʳ (refl⟩∘⟨ ×₁∘Δ) ⟩
+        ∇ ∘ (∇ ∘ ⟨ id , f ∘ f † ⟩) ×₁ f                                             ≈⟨ refl⟩∘⟨ ×₁-congʳ +-∇∘⟨⟩ ⟨
         ∇ ∘ (id + (f ∘ f †)) ×₁ f                                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ (+-comm id (f ∘ f †)) ⟩
         ∇ ∘ ((f ∘ f †) + id) ×₁ f                                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ f∘f†≤id ⟩
         ∇ ∘ id ×₁ f                                                                 ∎