Add semiadditive dagger categories

1 files changed, 287 insertions, 0 deletions

diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda
new file mode 100644
index 0000000..57d363e
--- /dev/null
+++ b/Category/Dagger/Semiadditive.agda
@@ -0,0 +1,287 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; suc; _⊔_)
+open import Categories.Category using (Category)
+
+module Category.Dagger.Semiadditive
+    {o ℓ e : Level}
+    (𝒞 : Category o ℓ e)
+  where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cocartesian 𝒞 using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open import Categories.Category.Dagger using (HasDagger)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (module Symmetric)
+open import Categories.Category.Monoidal.Symmetric.Properties using () renaming (module Shorthands to σ-Shorthands)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Object.Duality using (Coproduct⇒coProduct)
+
+record DaggerCocartesianMonoidal : Set (suc (o ⊔ ℓ ⊔ e)) where
+
+  field
+    cocartesian : Cocartesian
+    dagger : HasDagger 𝒞
+
+  open Cocartesian cocartesian using (i₁; i₂)
+  open CocartesianMonoidal cocartesian using (+-monoidal; _⊗₀_; _⊗₁_)
+  open CocartesianSymmetricMonoidal cocartesian using (+-symmetric)
+  open HasDagger dagger using (_†; isUnitary; isSelfAdjoint)
+  open Shorthands +-monoidal using (λ⇒; λ⇐; ρ⇒; ρ⇐; α⇒; α⇐)
+  open σ-Shorthands +-symmetric using (σ⇒)
+  open Category 𝒞
+
+  -- dagger and cocartesian monoidal structure are compatible
+  field
+    λ≅† : {A : Obj} → λ⇒ {A} † ≈ λ⇐
+    ρ≅† : {A : Obj} → ρ⇒ {A} † ≈ ρ⇐
+    α≅† : {A B C : Obj} → α⇒ {A} {B} {C} † ≈ α⇐
+    σ≅† : {A B : Obj} → σ⇒ {A} {B} † ≈ σ⇒
+    †-resp-⊗ : {A B C D : Obj} {f : A ⇒ B} {g : C ⇒ D} → (f ⊗₁ g) † ≈ (f †) ⊗₁ (g †)
+
+record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
+
+  field
+    daggerCocartesianMonoidal : DaggerCocartesianMonoidal
+
+  open DaggerCocartesianMonoidal daggerCocartesianMonoidal public
+  open CocartesianMonoidal cocartesian using (+-monoidal) renaming (_⊗₀_ to _⊕₀_; _⊗₁_ to _⊕₁_; ⊗ to ⊕) public
+
+  open Cocartesian cocartesian using (⊥; i₁; i₂; [_,_]; ¡; ∘[]; []∘+₁; []-cong₂; coproduct; ¡-unique; inject₁; inject₂; +-unique; +-g-η)
+  open CocartesianSymmetricMonoidal cocartesian using (+-symmetric)
+  open HasDagger dagger using (_†; †-involutive; †-resp-≈; †-identity; †-homomorphism)
+  open Monoidal +-monoidal using (unitorˡ-commute-from; unitorʳ-commute-from; assoc-commute-from; module unitorˡ; module unitorʳ; module associator)
+  open σ-Shorthands +-symmetric using (σ⇒)
+  open Symmetric +-symmetric using (module braiding)
+  open Shorthands +-monoidal using (λ⇒; λ⇐; ρ⇒; ρ⇐; α⇒; α⇐)
+  open Category 𝒞
+
+  -- projection maps
+  p₁ : {A B : Obj} → A ⊕₀ B ⇒ A
+  p₁ = i₁ †
+
+  p₂ : {A B : Obj} → A ⊕₀ B ⇒ B
+  p₂ = i₂ †
+
+  -- codiagonal
+  ▽ : {A : Obj} → A ⊕₀ A ⇒ A
+  ▽ = [ id , id ]
+
+  -- diagonal
+  △ : {A : Obj} → A ⇒ A ⊕₀ A
+  △ = ▽ †
+
+  private
+    op-binaryProducts : BinaryProducts op
+    op-binaryProducts = record { product = Coproduct⇒coProduct 𝒞 coproduct }
+    open BinaryProducts op-binaryProducts using () renaming (assocʳ∘⟨⟩ to []-assoc; swap∘⟨⟩ to []∘swap)
+
+  open ⊗-Reasoning +-monoidal
+  open ⇒-Reasoning 𝒞
+
+  ▽-assoc : {A : Obj} → ▽ {A} ∘ ▽ ⊕₁ id ≈ ▽ ∘ id ⊕₁ ▽ ∘ α⇒
+  ▽-assoc = begin
+      [ id , id ] ∘ [ id , id ] ⊕₁ id       ≈⟨ []∘+₁ ⟩
+      [ id ∘ [ id , id ] , id ∘ id ]        ≈⟨ []-cong₂ identityˡ identityˡ ⟩
+      [ [ id , id ] , id ]                  ≈⟨ []-assoc ⟨
+      [ id , [ id , id ] ] ∘ α⇒             ≈⟨ []-cong₂ identityˡ identityˡ ⟩∘⟨refl ⟨
+      [ id ∘ id , id ∘ [ id , id ] ] ∘ α⇒   ≈⟨ pushˡ (Equiv.sym []∘+₁) ⟩
+      [ id , id ] ∘ id ⊕₁ [ id , id ] ∘ α⇒  ∎
+
+  △-assoc : {A : Obj} → id ⊕₁ △ ∘ △ {A} ≈ α⇒ ∘ △ ⊕₁ id ∘ △
+  △-assoc = begin
+      id ⊕₁ △ ∘ △                 ≈⟨ †-involutive (id ⊕₁ △ ∘ △) ⟨
+      (id ⊕₁ △ ∘ △) † †           ≈⟨ †-resp-≈ †-homomorphism ⟩
+      (△ † ∘ (id ⊕₁ △) †) †       ≈⟨ †-resp-≈ (†-involutive ▽ ⟩∘⟨ †-resp-⊗) ⟩
+      (▽ ∘ (id †) ⊕₁ (△ †)) †     ≈⟨ †-resp-≈ (refl⟩∘⟨ †-identity ⟩⊗⟨ †-involutive ▽)⟩
+      (▽ ∘ id ⊕₁ ▽) †             ≈⟨ †-resp-≈ (refl⟩∘⟨ introʳ associator.isoʳ) ⟩
+      (▽ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ α⇐) †   ≈⟨ †-resp-≈ (refl⟩∘⟨ assoc ) ⟨
+      (▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ α⇐) † ≈⟨ †-resp-≈ (extendʳ ▽-assoc) ⟨
+      (▽ ∘ ▽ ⊕₁ id ∘ α⇐) †        ≈⟨ †-homomorphism ⟩
+      (▽ ⊕₁ id ∘ α⇐) † ∘ ▽ †      ≈⟨ pushˡ †-homomorphism ⟩
+      α⇐ † ∘ (▽ ⊕₁ id) † ∘ △      ≈⟨ †-resp-≈ α≅† ⟩∘⟨refl ⟨
+      α⇒ † † ∘ (▽ ⊕₁ id) † ∘ △    ≈⟨ †-involutive α⇒ ⟩∘⟨refl ⟩
+      α⇒ ∘ (▽ ⊕₁ id) † ∘ △        ≈⟨ refl⟩∘⟨ †-resp-⊗ ⟩∘⟨refl ⟩
+      α⇒ ∘ (▽ †) ⊕₁ (id †) ∘ △    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ †-identity ⟩∘⟨refl ⟩
+      α⇒ ∘ △ ⊕₁ id ∘ △            ∎
+
+  ! : {A : Obj} → A ⇒ ⊥
+  ! = ¡ †
+
+  ▽-identityˡ : {A : Obj} → ▽ {A} ∘ ¡ ⊕₁ id ≈ λ⇒
+  ▽-identityˡ = begin
+      [ id , id ] ∘ ¡ ⊕₁ id ≈⟨ []∘+₁ ⟩
+      [ id ∘ ¡ , id ∘ id ]  ≈⟨ []-cong₂ identityˡ identity² ⟩
+      [ ¡ , id ]            ∎
+
+  △-identityˡ : {A : Obj} → ! {A} ⊕₁ id ∘ △ ≈ λ⇐
+  △-identityˡ = begin
+      ! ⊕₁ id ∘ △           ≈⟨ refl⟩⊗⟨ †-identity ⟩∘⟨refl ⟨
+      (¡ †) ⊕₁ (id †) ∘ ▽ † ≈⟨ †-resp-⊗ ⟩∘⟨refl ⟨
+      (¡ ⊕₁ id) † ∘ ▽ †     ≈⟨ †-homomorphism ⟨
+      (▽ ∘ ¡ ⊕₁ id) †       ≈⟨ †-resp-≈ ▽-identityˡ ⟩
+      λ⇒ †                  ≈⟨ λ≅† ⟩
+      λ⇐ ∎
+
+  ▽-identityʳ : {A : Obj} → ▽ {A} ∘ id ⊕₁ ¡ ≈ ρ⇒
+  ▽-identityʳ = begin
+      [ id , id ] ∘ id ⊕₁ ¡ ≈⟨ []∘+₁ ⟩
+      [ id ∘ id , id ∘ ¡ ]  ≈⟨ []-cong₂ identity² identityˡ ⟩
+      [ id , ¡ ]            ∎
+
+  △-identityʳ : {A : Obj} → id {A} ⊕₁ ! ∘ △ ≈ ρ⇐
+  △-identityʳ = begin
+      id ⊕₁ (¡ †) ∘ ▽ †     ≈⟨ †-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
+      (id †) ⊕₁ (¡ †) ∘ ▽ † ≈⟨ †-resp-⊗ ⟩∘⟨refl ⟨
+      (id ⊕₁ ¡) † ∘ ▽ †     ≈⟨ †-homomorphism ⟨
+      (▽ ∘ id ⊕₁ ¡) †       ≈⟨ †-resp-≈ ▽-identityʳ ⟩
+      ρ⇒ †                  ≈⟨ ρ≅† ⟩
+      ρ⇐                    ∎
+
+  ▽-comm : {A : Obj} → ▽ {A} ∘ σ⇒ ≈ ▽
+  ▽-comm = []∘swap
+
+  △-comm : {A : Obj} → σ⇒ ∘ △ {A} ≈ △
+  △-comm = begin
+      σ⇒ ∘ ▽ †    ≈⟨ σ≅† ⟩∘⟨refl ⟨
+      σ⇒ † ∘ ▽ †  ≈⟨ †-homomorphism ⟨
+      (▽ ∘ σ⇒) †  ≈⟨ †-resp-≈ ▽-comm ⟩
+      ▽ †         ∎
+
+  ⇒▽ : {A B : Obj} {f : A ⇒ B} → f ∘ ▽ ≈ ▽ ∘ f ⊕₁ f
+  ⇒▽ {A} {B} {f} = begin
+      f ∘ [ id , id ]       ≈⟨ ∘[] ⟩
+      [ f ∘ id , f ∘ id ]   ≈⟨ []-cong₂ identityʳ identityʳ ⟩
+      [ f , f ]             ≈⟨ []-cong₂ identityˡ identityˡ ⟨
+      [ id ∘ f , id ∘ f ]   ≈⟨ []∘+₁ ⟨
+      [ id , id ] ∘ f ⊕₁ f  ∎
+
+  ⇒△ : {A B : Obj} {f : A ⇒ B} → △ ∘ f ≈ f ⊕₁ f ∘ △
+  ⇒△ {A} {B} {f} = begin
+      ▽ † ∘ f                   ≈⟨ refl⟩∘⟨ †-involutive f ⟨
+      ▽ † ∘ f † †               ≈⟨ †-homomorphism ⟨
+      (f † ∘ ▽) †               ≈⟨ †-resp-≈ ⇒▽ ⟩
+      (▽ ∘ (f †) ⊕₁ (f †)) †    ≈⟨ †-homomorphism ⟩
+      ((f †) ⊕₁ (f †)) † ∘ ▽ †  ≈⟨ †-resp-⊗ ⟩∘⟨refl ⟩
+      (f † †) ⊕₁ (f † †) ∘ ▽ †  ≈⟨ †-involutive f ⟩⊗⟨ †-involutive f ⟩∘⟨refl ⟩
+      f ⊕₁ f ∘ ▽ †              ∎
+
+  ⇒¡ : {A B : Obj} {f : A ⇒ B} → f ∘ ¡ ≈ ¡
+  ⇒¡ {A} {B} {f} = Equiv.sym (¡-unique (f ∘ ¡))
+
+  ⇒! : {A B : Obj} {f : A ⇒ B} → ! ∘ f ≈ !
+  ⇒! {A} {B} {f} = begin
+      ¡ † ∘ f     ≈⟨ refl⟩∘⟨ †-involutive f ⟨
+      ¡ † ∘ f † † ≈⟨ †-homomorphism ⟨
+      (f † ∘ ¡) † ≈⟨ †-resp-≈ ⇒¡ ⟩
+      ¡ †         ∎
+
+  ρ⇐≈i₁ : {A : Obj} → ρ⇐ {A} ≈ i₁
+  ρ⇐≈i₁ = Equiv.refl
+
+  λ⇐≈i₂ : {A : Obj} → λ⇐ {A} ≈ i₂
+  λ⇐≈i₂ = Equiv.refl
+
+  λ⇒≈p₂ : {A : Obj} → λ⇒ {A} ≈ p₂
+  λ⇒≈p₂ = begin
+      λ⇒      ≈⟨ †-involutive λ⇒ ⟨
+      λ⇒ † †  ≈⟨ †-resp-≈ λ≅† ⟩
+      λ⇐ †    ≈⟨ †-resp-≈ λ⇐≈i₂ ⟩
+      i₂ †    ∎
+
+  ρ⇒≈p₁ : {A : Obj} → ρ⇒ {A} ≈ p₁
+  ρ⇒≈p₁ = begin
+      ρ⇒      ≈⟨ †-involutive ρ⇒ ⟨
+      ρ⇒ † †  ≈⟨ †-resp-≈ ρ≅† ⟩
+      ρ⇐ †    ≈⟨ †-resp-≈ ρ⇐≈i₁ ⟩
+      i₁ †    ∎
+
+  i₁-⊕ : {A B : Obj} → i₁ {A} {B} ≈ id ⊕₁ ¡ ∘ ρ⇐
+  i₁-⊕ = begin
+      i₁            ≈⟨ identityʳ ⟨
+      i₁ ∘ id       ≈⟨ inject₁ ⟨
+      id ⊕₁ ¡ ∘ i₁  ≈⟨ refl⟩∘⟨ ρ⇐≈i₁ ⟨
+      id ⊕₁ ¡ ∘ ρ⇐  ∎
+
+  i₂-⊕ : {A B : Obj} → i₂ {A} {B} ≈ ¡ ⊕₁ id ∘ λ⇐
+  i₂-⊕ = begin
+      i₂            ≈⟨ identityʳ ⟨
+      i₂ ∘ id       ≈⟨ inject₂ ⟨
+      ¡ ⊕₁ id ∘ i₂  ≈⟨ refl⟩∘⟨ λ⇐≈i₂ ⟨
+      ¡ ⊕₁ id ∘ λ⇐  ∎
+
+  p₁-⊕ : {A B : Obj} → p₁ {A} {B} ≈ ρ⇒ ∘ id ⊕₁ !
+  p₁-⊕ {A} {B} = begin
+      i₁ †                      ≈⟨ †-resp-≈ i₁-⊕ ⟩
+      (id ⊕₁ ¡ ∘ ρ⇐) †          ≈⟨ †-homomorphism ⟩
+      ρ⇐ † ∘ (id ⊕₁ ¡) †        ≈⟨ refl⟩∘⟨ †-resp-⊗ ⟩
+      ρ⇐ † ∘ (id †) ⊕₁ (¡ †)    ≈⟨ †-resp-≈ ρ≅† ⟩∘⟨refl ⟨
+      ρ⇒ † † ∘ (id †) ⊕₁ (¡ †)  ≈⟨ †-involutive ρ⇒ ⟩∘⟨ †-identity ⟩⊗⟨refl ⟩
+      ρ⇒ ∘ id ⊕₁ (¡ †)          ∎
+
+  p₂-⊕ : {A B : Obj} → p₂ {A} {B} ≈ λ⇒ ∘ ! ⊕₁ id
+  p₂-⊕ {A} {B} = begin
+      i₂ †                      ≈⟨ †-resp-≈ i₂-⊕ ⟩
+      (¡ ⊕₁ id ∘ λ⇐) †          ≈⟨ †-homomorphism ⟩
+      λ⇐ † ∘ (¡ ⊕₁ id) †        ≈⟨ refl⟩∘⟨ †-resp-⊗ ⟩
+      λ⇐ † ∘ (¡ †) ⊕₁ (id †)    ≈⟨ †-resp-≈ λ≅† ⟩∘⟨refl ⟨
+      λ⇒ † † ∘ (¡ †) ⊕₁ (id †)  ≈⟨ †-involutive λ⇒ ⟩∘⟨ refl⟩⊗⟨ †-identity ⟩
+      λ⇒ ∘ (¡ †) ⊕₁ id          ∎
+
+  -- zero arrows
+  z : {A B : Obj} → A ⇒ B
+  z = ¡ ∘ !
+
+  field
+    -- orthogonality conditions: pᵢiⱼ ≈ δᵢⱼ
+    p₁-i₁ : {A B : Obj} → p₁ {A} {B} ∘ i₁ ≈ id {A}
+    p₂-i₂ : {A B : Obj} → p₂ {A} {B} ∘ i₂ ≈ id {B}
+    p₂-i₁ : {A B : Obj} → p₂ {A} {B} ∘ i₁ ≈ z {A} {B}
+    p₁-i₂ : {A B : Obj} → p₁ {A} {B} ∘ i₂ ≈ z {B} {A}
+
+  -- commutative monoid structure on homs
+  module _ {A B : Obj} where
+
+    _+_ : A ⇒ B → A ⇒ B → A ⇒ B
+    _+_ f g = ▽ ∘ f ⊕₁ g ∘ △
+
+    +-associative : {f g h : A ⇒ B} → (f + g) + h ≈ f + (g + h)
+    +-associative {f} {g} {h} = begin
+        ▽ ∘ (▽ ∘ f ⊕₁ g ∘ △) ⊕₁ h ∘ △                     ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
+        ▽ ∘ ▽ ⊕₁ id ∘ (f ⊕₁ g ∘ △) ⊕₁ h ∘ △               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩
+        ▽ ∘ ▽ ⊕₁ id ∘ (f ⊕₁ g) ⊕₁ h ∘ △ ⊕₁ id ∘ △         ≈⟨ extendʳ ▽-assoc ⟩
+        ▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ (f ⊕₁ g) ⊕₁ h ∘ △ ⊕₁ id ∘ △  ≈⟨ refl⟩∘⟨ pullʳ (extendʳ assoc-commute-from) ⟩
+        ▽ ∘ id ⊕₁ ▽ ∘ f ⊕₁ g ⊕₁ h ∘ α⇒ ∘ △ ⊕₁ id ∘ △      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-assoc ⟨
+        ▽ ∘ id ⊕₁ ▽ ∘ f ⊕₁ g ⊕₁ h ∘ id ⊕₁ △ ∘ △           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ʳ ⟩
+        ▽ ∘ id ⊕₁ ▽ ∘ f ⊕₁ (g ⊕₁ h ∘ △) ∘ △               ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        ▽ ∘ f ⊕₁ (▽ ∘ g ⊕₁ h ∘ △) ∘ △                     ∎
+
+    +-identityˡ : {f : A ⇒ B} → z + f ≈ f
+    +-identityˡ {f} = begin
+        ▽ ∘ (¡ ∘ !) ⊕₁ f ∘ △        ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
+        ▽ ∘ ¡ ⊕₁ id ∘ ! ⊕₁ f ∘ △    ≈⟨ pullˡ ▽-identityˡ ⟩
+        λ⇒ ∘ ! ⊕₁ f ∘ △             ≈⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
+        λ⇒ ∘ id ⊕₁ f ∘ ! ⊕₁ id ∘ △  ≈⟨ extendʳ unitorˡ-commute-from ⟩
+        f ∘ λ⇒ ∘ ! ⊕₁ id ∘ △        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityˡ ⟩
+        f ∘ λ⇒ ∘ λ⇐                 ≈⟨ elimʳ unitorˡ.isoʳ ⟩
+        f                           ∎
+
+    +-identityʳ : {f : A ⇒ B} → f + z ≈ f
+    +-identityʳ {f} = begin
+        ▽ ∘ f ⊕₁ (¡ ∘ !) ∘ △        ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        ▽ ∘ id ⊕₁ ¡ ∘ (f ⊕₁ !) ∘ △  ≈⟨ pullˡ ▽-identityʳ ⟩
+        ρ⇒ ∘ f ⊕₁ ! ∘ △             ≈⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
+        ρ⇒ ∘ f ⊕₁ id ∘ id ⊕₁ ! ∘ △  ≈⟨ extendʳ unitorʳ-commute-from ⟩
+        f ∘ ρ⇒ ∘ id ⊕₁ ! ∘ △        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityʳ ⟩
+        f ∘ ρ⇒ ∘ ρ⇐                 ≈⟨ elimʳ unitorʳ.isoʳ ⟩
+        f ∎
+
+    +-commutative : {f g : A ⇒ B} → f + g ≈ g + f
+    +-commutative {f} {g} = begin
+        ▽ ∘ f ⊕₁ g ∘ △      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ △-comm ⟨
+        ▽ ∘ f ⊕₁ g ∘ σ⇒ ∘ △ ≈⟨ refl⟩∘⟨ extendʳ (braiding.⇒.sym-commute _) ⟩
+        ▽ ∘ σ⇒ ∘ g ⊕₁ f ∘ △ ≈⟨ pullˡ ▽-comm ⟩
+        ▽ ∘ g ⊕₁ f ∘ △      ∎