diff options
| -rw-r--r-- | Category/Monoidal/Instance/Posets.agda | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/Category/Monoidal/Instance/Posets.agda b/Category/Monoidal/Instance/Posets.agda new file mode 100644 index 0000000..ad7363e --- /dev/null +++ b/Category/Monoidal/Instance/Posets.agda @@ -0,0 +1,84 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Category.Monoidal.Instance.Posets {c ℓ₁ ℓ₂ : Level} where + +open import Categories.Category.Instance.Posets using (Posets) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.Morphism (Posets c ℓ₁ ℓ₂) using (_≅_) +open import Data.Product using (_,_; map; proj₁; proj₂; assocʳ′; assocˡ′) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-poset) +open import Data.Unit.Polymorphic using (⊤; tt) +open import Relation.Binary using (Poset) +open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo) + +open Poset using (module Eq) +open PosetHomomorphism using (⟦_⟧; mono) + +private + + ⊗ : Bifunctor (Posets c ℓ₁ ℓ₂) (Posets c ℓ₁ ℓ₂) (Posets c ℓ₁ ℓ₂) + ⊗ = record + { F₀ = λ (P , Q) → ×-poset P Q + ; F₁ = λ (f , g) → mkPosetHomo _ _ (map ⟦ f ⟧ ⟦ g ⟧) (map (mono f) (mono g)) + ; identity = λ { {x , y} → Eq.refl x , Eq.refl y } + ; homomorphism = λ { {_} {_} {e , f} → Eq.refl e , Eq.refl f } + ; F-resp-≈ = λ (x , y) → x , y + } + + unit : Poset c ℓ₁ ℓ₂ + unit = record + { Carrier = ⊤ + ; _≈_ = λ _ _ → ⊤ + ; _≤_ = λ _ _ → ⊤ + ; isPartialOrder = _ + } + + unitorˡ : {X : Poset c ℓ₁ ℓ₂} → ×-poset unit X ≅ X + unitorˡ {X} = record + { from = mkPosetHomo _ _ proj₂ proj₂ + ; to = mkPosetHomo _ _ (tt ,_) (tt ,_) + ; iso = record + { isoˡ = tt , Eq.refl X + ; isoʳ = Eq.refl X + } + } + + unitorʳ : {X : Poset c ℓ₁ ℓ₂} → ×-poset X unit ≅ X + unitorʳ {X} = record + { from = mkPosetHomo _ _ proj₁ proj₁ + ; to = mkPosetHomo _ _ (_, tt) (_, tt) + ; iso = record + { isoˡ = Eq.refl X , tt + ; isoʳ = Eq.refl X + } + } + + associator : {X Y Z : Poset c ℓ₁ ℓ₂} → ×-poset (×-poset X Y) Z ≅ ×-poset X (×-poset Y Z) + associator {X} {Y} {Z} = record + { from = mkPosetHomo _ _ assocʳ′ assocʳ′ + ; to = mkPosetHomo _ _ assocˡ′ assocˡ′ + ; iso = record + { isoˡ = (Eq.refl X , Eq.refl Y) , Eq.refl Z + ; isoʳ = Eq.refl X , (Eq.refl Y , Eq.refl Z) + } + } + +Posets-Monoidal : Monoidal (Posets c ℓ₁ ℓ₂) +Posets-Monoidal = record + { ⊗ = ⊗ + ; unit = unit + ; unitorˡ = unitorˡ + ; unitorʳ = unitorʳ + ; associator = associator + ; unitorˡ-commute-from = λ {_ X} → Eq.refl X + ; unitorˡ-commute-to = λ {_ Y} → tt , Eq.refl Y + ; unitorʳ-commute-from = λ {_ X} → Eq.refl X + ; unitorʳ-commute-to = λ {_ Y} → Eq.refl Y , tt + ; assoc-commute-from = λ {_ A _ _ B _ _ C} → Eq.refl A , Eq.refl B , Eq.refl C + ; assoc-commute-to = λ {_ A _ _ B _ _ C} → (Eq.refl A , Eq.refl B) , Eq.refl C + ; triangle = λ {X Y} → Eq.refl X , Eq.refl Y + ; pentagon = λ {W X Y Z} → Eq.refl W , Eq.refl X , Eq.refl Y , Eq.refl Z + } |