diff options
Diffstat (limited to 'Category/Dagger/2-Poset.agda')
| -rw-r--r-- | Category/Dagger/2-Poset.agda | 49 |
1 files changed, 10 insertions, 39 deletions
diff --git a/Category/Dagger/2-Poset.agda b/Category/Dagger/2-Poset.agda index 27c01af..fcd7e4a 100644 --- a/Category/Dagger/2-Poset.agda +++ b/Category/Dagger/2-Poset.agda @@ -1,7 +1,6 @@ {-# 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 @@ -17,7 +16,7 @@ open import Categories.Enriched.Category Posets-Monoidal using () renaming (Cate 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 import Relation.Binary.Morphism.Bundles using (PosetHomomorphism) open PosetHomomorphism using (⟦_⟧; cong; mono) @@ -51,49 +50,13 @@ record Dagger-2-Poset : Set (suc (o ⊔ ℓ ⊔ e)) where private module P {A B : Obj} = Poset (hom A B) - open P using (_≤_) public + open P using (_≤_; reflexive) public open Category category hiding (Obj) public open HasDagger hasDagger 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 𝒞 - module _ (S : Dagger-2-Poset) where open Dagger-2-Poset S @@ -104,6 +67,14 @@ module _ (S : Dagger-2-Poset) where functional : f ∘ f † ≤ id entire : id ≤ f † ∘ f + open import Categories.Morphism category using (Iso) + + unitary-isMap : {A B : Obj} {f : A ⇒ B} → Iso f (f †) → IsMap f + unitary-isMap iso = let open Iso iso in record + { functional = reflexive isoʳ + ; entire = reflexive (Equiv.sym isoˡ) + } + record Map (A B : Obj) : Set (ℓ ⊔ e) where field |