diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/Dagger/2-Poset.agda | 95 | ||||
| -rw-r--r-- | Category/Dagger/Semiadditive.agda | 73 |
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 |