From 7cb4f160835178d06e0c0bf9802c3cad6d48a9d0 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sun, 11 Oct 2026 22:59:21 -0700
Subject: Add hom-set addition to semiadditive record

---
 Category/Dagger/Semiadditive.agda | 37 ++++++++++++++++++++-----------------
 1 file changed, 20 insertions(+), 17 deletions(-)

(limited to 'Category/Dagger/Semiadditive.agda')

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
-- 
cgit v1.2.3