Define dagger-2-posets

2 files changed, 166 insertions, 2 deletions

diff --git a/Category/Dagger/2-Poset.agda b/Category/Dagger/2-Poset.agda
new file mode 100644
index 0000000..136a63e
--- /dev/null
+++ b/Category/Dagger/2-Poset.agda
@@ -0,0 +1,95 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
+open import Level using (Level; suc; _⊔_)
+
+module Category.Dagger.2-Poset {o ℓ e : Level} where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+
+open import Category.Monoidal.Instance.Posets {ℓ} {e} {e} using (Posets-Monoidal)
+
+open import Categories.Category.Dagger using (HasDagger)
+open import Categories.Category.Helper using (categoryHelper)
+open import Categories.Category.Instance.Posets using (Posets)
+open import Categories.Enriched.Category Posets-Monoidal using () renaming (Category to 2-Poset)
+open import Data.Product using (_,_)
+open import Data.Unit.Polymorphic using (tt)
+open import Relation.Binary using (Poset)
+open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)
+
+open PosetHomomorphism using (⟦_⟧; cong)
+
+record Dagger-2-Poset : Set (suc (o ⊔ ℓ ⊔ e)) where
+
+  open Poset using (Carrier; _≈_; isEquivalence)
+
+  field
+    2-poset : 2-Poset o
+
+  open 2-Poset 2-poset
+
+  category : Category o ℓ e
+  category = categoryHelper record
+      { Obj = Obj
+      ; _⇒_ = λ A B → Carrier (hom A B)
+      ; _≈_ = λ {A B} → _≈_ (hom A B)
+      ; id = ⟦ id ⟧ tt
+      ; _∘_ = λ f g → ⟦ ⊚ ⟧ (f , g)
+      ; assoc = ⊚-assoc
+      ; identityˡ = unitˡ
+      ; identityʳ = unitʳ
+      ; equiv = λ {A B} → isEquivalence (hom A B)
+      ; ∘-resp-≈ = λ f≈h g≈i → cong ⊚ (f≈h , g≈i)
+      }
+
+  field
+    hasDagger : HasDagger category
+
+  private
+    module P {A B : Obj} = Poset (hom A B)
+
+  open P using (_≤_) public
+  open Category category using (_⇒_) public
+  open HasDagger hasDagger using (_†) public
+
+  field
+    †-resp-≤ : {A B : Obj} {f g : A ⇒ B} → f ≤ g → f † ≤ g †
+
+dagger-2-poset : {𝒞 : Category o ℓ e} (ISA† : IdempotentSemiadditiveDagger 𝒞) → Dagger-2-Poset
+dagger-2-poset {𝒞} ISA† = record
+    { 2-poset = record
+        { Obj = Obj
+        ; hom = λ A B → record
+            { Carrier = A ⇒ B
+            ; _≈_ = _≈_
+            ; _≤_ = ISA†._≤_
+            ; isPartialOrder = record
+                { isPreorder = record
+                    { isEquivalence = equiv
+                    ; reflexive = λ x≈y → Equiv.trans (ISA†.+-congʳ x≈y) ISA†.≤-refl
+                    ; trans = ISA†.≤-trans
+                    }
+                ; antisym = ISA†.≤-antisym
+                }
+            }
+        ; id = mkPosetHomo _ _ (λ _ → id) (λ _ → ISA†.≤-refl)
+        ; ⊚ = mkPosetHomo _ _ (λ (f , g) → f ∘ g) (λ (≤₁ , ≤₂) → ISA†.≤-resp-∘ ≤₁ ≤₂)
+        ; ⊚-assoc = assoc
+        ; unitˡ = identityˡ
+        ; unitʳ = identityʳ
+        }
+    ; hasDagger = record
+        { _† = ISA†._†
+        ; †-identity = ISA†.†-identity
+        ; †-homomorphism = ISA†.†-homomorphism
+        ; †-resp-≈ = ISA†.⟨_⟩†
+        ; †-involutive = ISA†.†-involutive
+        }
+    ; †-resp-≤ = ISA†.†-resp-≤
+    }
+  where
+    module ISA† = IdempotentSemiadditiveDagger ISA†
+    open Category 𝒞
+    open ⊗-Reasoning ISA†.+-monoidal
diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda
index 980f195..283f270 100644
--- a/Category/Dagger/Semiadditive.agda
+++ b/Category/Dagger/Semiadditive.agda
@@ -19,6 +19,7 @@ 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)
+open import Relation.Binary using (Rel)
 
 record DaggerCocartesianMonoidal : Set (suc (o ⊔ ℓ ⊔ e)) where
 
@@ -277,6 +278,8 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
     _+_ : A ⇒ B → A ⇒ B → A ⇒ B
     _+_ f g = ▽ ∘ f ⊕₁ g ∘ △
 
+    infixl 6 _+_
+
     +-associative : {f g h : A ⇒ B} → (f + g) + h ≈ f + (g + h)
     +-associative {f} {g} {h} = begin
         ▽ ∘ (▽ ∘ f ⊕₁ g ∘ △) ⊕₁ h ∘ △                     ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
@@ -315,6 +318,36 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
         ▽ ∘ σ⇒ ∘ g ⊕₁ f ∘ △ ≈⟨ pullˡ ▽-comm ⟩
         ▽ ∘ g ⊕₁ f ∘ △      ∎
 
+    +-cong : {f g h i : A ⇒ B} → f ≈ h → g ≈ i → f + g ≈ h + i
+    +-cong f≈h g≈i = refl⟩∘⟨ f≈h ⟩⊗⟨ g≈i ⟩∘⟨refl
+
+    +-congˡ : {f g i : A ⇒ B} → g ≈ i → f + g ≈ f + i
+    +-congˡ g≈i = +-cong Equiv.refl g≈i
+
+    +-congʳ : {f g h : A ⇒ B} → f ≈ h → f + g ≈ h + g
+    +-congʳ f≈h = +-cong f≈h Equiv.refl
+
+  +-† : {A B : Obj} {f g : A ⇒ B} → (f + g) † ≈ (f †) + (g †)
+  +-† {f = f} {g} = begin
+      (▽ ∘ f ⊕₁ g ∘ △) †     ≈⟨ †-homomorphism ⟩
+      (f ⊕₁ g ∘ △) † ∘ ▽ †   ≈⟨ pushˡ †-homomorphism ⟩
+      △ † ∘ (f ⊕₁ g) † ∘ ▽ † ≈⟨ †-involutive ▽ ⟩∘⟨refl ⟩
+      ▽ ∘ (f ⊕₁ g) † ∘ △     ≈⟨ refl⟩∘⟨ †-resp-⊗ ⟩∘⟨refl ⟩
+      ▽ ∘ (f †) ⊕₁ (g †) ∘ △ ∎
+
+  -- bilinearity of composition
+  ∘-distribˡ : {A B C : Obj} {f : B ⇒ C} {g h : A ⇒ B} → f ∘ (g + h) ≈ f ∘ g + f ∘ h
+  ∘-distribˡ {f = f} {g} {h} = begin
+      f ∘ ▽ ∘ g ⊕₁ h ∘ △          ≈⟨ extendʳ ⇒▽ ⟩
+      ▽ ∘ f ⊕₁ f ∘ g ⊕₁ h ∘ △     ≈⟨ refl⟩∘⟨ pullˡ (Equiv.sym ⊗-distrib-over-∘) ⟩
+      ▽ ∘ (f ∘ g) ⊕₁ (f ∘ h) ∘ △  ∎
+
+  ∘-distribʳ : {A B C : Obj} {f g : B ⇒ C} {h : A ⇒ B} → (f + g) ∘ h ≈ f ∘ h + g ∘ h
+  ∘-distribʳ {f = f} {g} {h} = begin
+      (▽ ∘ f ⊕₁ g ∘ △) ∘ h        ≈⟨ pullʳ (pullʳ ⇒△) ⟩
+      ▽ ∘ f ⊕₁ g ∘ h ⊕₁ h ∘ △     ≈⟨ refl⟩∘⟨ pullˡ (Equiv.sym ⊗-distrib-over-∘) ⟩
+      ▽ ∘ (f ∘ h) ⊕₁ (g ∘ h) ∘ △  ∎
+
 record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
 
   field
@@ -329,8 +362,6 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
   field
     idempotent : {A B : Obj} {f : A ⇒ B} → f + f ≈ f
 
-  open import Relation.Binary using (Rel)
-
   _≤_ : {A B : Obj} → Rel (A ⇒ B) e
   _≤_ {A} {B} f g = f + g ≈ g
 
@@ -352,6 +383,44 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       g + h       ≈⟨ g≤h ⟩
       h           ∎
 
+  ≤-resp-+
+      : {A B : Obj}
+        {f g h i : A ⇒ B}
+      → f ≤ h
+      → g ≤ i
+      → (f + g) ≤ (h + i)
+  ≤-resp-+ {f = f} {g} {h} {i} f≤h g≤i = begin
+      f + g + (h + i)   ≈⟨ +-associative ⟩
+      f + (g + (h + i)) ≈⟨ +-congˡ +-associative ⟨
+      f + (g + h + i)   ≈⟨ +-congˡ (+-congʳ +-commutative) ⟩
+      f + (h + g + i)   ≈⟨ +-congˡ +-associative ⟩
+      f + (h + (g + i)) ≈⟨ +-associative ⟨
+      f + h + (g + i)   ≈⟨ +-cong f≤h g≤i ⟩
+      h + i             ∎
+
+  ≤-resp-∘
+      : {A B C : Obj}
+        {f h : B ⇒ C}
+        {g i : A ⇒ B}
+      → f ≤ h
+      → g ≤ i
+      → (f ∘ g) ≤ (h ∘ i)
+  ≤-resp-∘ {f = f} {h} {g} {i} f≤h g≤i = begin
+      f ∘ g + (h ∘ i)         ≈⟨ +-congˡ (f≤h ⟩∘⟨refl) ⟨
+      f ∘ g + ((f + h) ∘ i)   ≈⟨ +-congˡ ∘-distribʳ ⟩
+      f ∘ g + (f ∘ i + h ∘ i) ≈⟨ +-associative ⟨
+      f ∘ g + f ∘ i + h ∘ i   ≈⟨ +-congʳ ∘-distribˡ ⟨
+      f ∘ (g + i) + h ∘ i     ≈⟨ +-congʳ (refl⟩∘⟨ g≤i) ⟩
+      f ∘ i + h ∘ i           ≈⟨ ∘-distribʳ ⟨
+      (f + h) ∘ i             ≈⟨ f≤h ⟩∘⟨refl ⟩
+      h ∘ i                   ∎
+
+  †-resp-≤ : {A B : Obj} {f g : A ⇒ B} → f ≤ g → (f †) ≤ (g †)
+  †-resp-≤ {A} {B} {f} {g} f≤g = begin
+      (f †) + (g †) ≈⟨ +-† ⟨
+      (f + g) †     ≈⟨ ⟨ f≤g ⟩† ⟩
+      g †           ∎
+
   -- special law
   ▽∘△ : {A : Obj} → ▽ ∘ △ ≈ id {A}
   ▽∘△ = begin