diff options
| -rw-r--r-- | Category/Instance/MonoidalPreorders.agda | 4 | ||||
| -rw-r--r-- | Category/Instance/SymMonPre.agda | 73 | ||||
| -rw-r--r-- | Preorder/Monoidal.agda | 23 |
3 files changed, 96 insertions, 4 deletions
diff --git a/Category/Instance/MonoidalPreorders.agda b/Category/Instance/MonoidalPreorders.agda index 6bdeb3f..6f8ffe0 100644 --- a/Category/Instance/MonoidalPreorders.agda +++ b/Category/Instance/MonoidalPreorders.agda @@ -71,5 +71,5 @@ MonoidalPreorders c ℓ e = categoryHelper record ; ∘-resp-≈ = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i) } where - open MonoidalMonotone using (F; cong) - open MonoidalPreorder using (U; refl; module Eq) + open MonoidalMonotone using (cong) + open MonoidalPreorder using (refl; module Eq) diff --git a/Category/Instance/SymMonPre.agda b/Category/Instance/SymMonPre.agda new file mode 100644 index 0000000..a792c6d --- /dev/null +++ b/Category/Instance/SymMonPre.agda @@ -0,0 +1,73 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Instance.SymMonPre where + +import Category.Instance.MonoidalPreorders as MP using (_≗_; module ≗) + +open import Categories.Category using (Category) +open import Categories.Category.Helper using (categoryHelper) +open import Category.Instance.MonoidalPreorders using (MonoidalPreorders) +open import Level using (Level; suc; _⊔_) +open import Preorder.Monoidal using (SymmetricMonoidalPreorder; SymmetricMonoidalMonotone) +open import Relation.Binary using (IsEquivalence) + +private + + identity : {c ℓ e : Level} (A : SymmetricMonoidalPreorder c ℓ e) → SymmetricMonoidalMonotone A A + identity {c} {ℓ} {e} A = record + { monoidalMonotone = id {monoidalPreorder} + } + where + open SymmetricMonoidalPreorder A using (monoidalPreorder) + open Category (MonoidalPreorders c ℓ e) using (id) + + compose + : {c ℓ e : Level} + {P Q R : SymmetricMonoidalPreorder c ℓ e} + → SymmetricMonoidalMonotone Q R + → SymmetricMonoidalMonotone P Q + → SymmetricMonoidalMonotone P R + compose {c} {ℓ} {e} {R = R} G F = record + { monoidalMonotone = G.monoidalMonotone ∘ F.monoidalMonotone + } + where + module G = SymmetricMonoidalMonotone G + module F = SymmetricMonoidalMonotone F + open Category (MonoidalPreorders c ℓ e) using (_∘_) + +module _ {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} {A : SymmetricMonoidalPreorder c₁ ℓ₁ e₁} {B : SymmetricMonoidalPreorder c₂ ℓ₂ e₂} where + + open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) + + -- Pointwise equality of symmetric monoidal monotone maps + _≗_ : (f g : SymmetricMonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂) + f ≗ g = mM f MP.≗ mM g + + infix 4 _≗_ + + ≗-isEquivalence : IsEquivalence _≗_ + ≗-isEquivalence = let open MP.≗ in record + { refl = λ {x} → refl {x = mM x} + ; sym = λ {f g} → sym {x = mM f} {y = mM g} + ; trans = λ {f g h} → trans {i = mM f} {j = mM g} {k = mM h} + } + + module ≗ = IsEquivalence ≗-isEquivalence + +-- The category of symmetric monoidal preorders +SymMonPre : (c ℓ e : Level) → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ) +SymMonPre c ℓ e = categoryHelper record + { Obj = SymmetricMonoidalPreorder c ℓ e + ; _⇒_ = SymmetricMonoidalMonotone + ; _≈_ = _≗_ + ; id = λ {A} → identity A + ; _∘_ = λ {A B C} f g → compose f g + ; assoc = λ {_ _ _ D _ _ _ _} → Eq.refl D + ; identityˡ = λ {_ B _ _} → Eq.refl B + ; identityʳ = λ {_ B _ _} → Eq.refl B + ; equiv = ≗-isEquivalence + ; ∘-resp-≈ = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i) + } + where + open SymmetricMonoidalMonotone using (cong) + open SymmetricMonoidalPreorder using (refl; module Eq) diff --git a/Preorder/Monoidal.agda b/Preorder/Monoidal.agda index 02c6d88..34763c7 100644 --- a/Preorder/Monoidal.agda +++ b/Preorder/Monoidal.agda @@ -67,6 +67,9 @@ record SymmetricMonoidalPreorder (c ℓ e : Level) : Set (suc (c ⊔ ℓ ⊔ e)) monoidal : Monoidal U symmetric : Symmetric monoidal + monoidalPreorder : MonoidalPreorder c ℓ e + monoidalPreorder = record { monoidal = monoidal } + open Preorder U public open Monoidal monoidal public open Symmetric symmetric public @@ -77,8 +80,9 @@ record MonoidalMonotone (Q : MonoidalPreorder c₂ ℓ₂ e₂) : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₁ ⊔ e₂) where - module P = MonoidalPreorder P - module Q = MonoidalPreorder Q + private + module P = MonoidalPreorder P + module Q = MonoidalPreorder Q field F : PreorderHomomorphism P.U Q.U @@ -88,3 +92,18 @@ record MonoidalMonotone field ε : Q.unit Q.≲ ⟦ P.unit ⟧ ⊗-homo : (p₁ p₂ : P.Carrier) → ⟦ p₁ ⟧ Q.⊗ ⟦ p₂ ⟧ Q.≲ ⟦ p₁ P.⊗ p₂ ⟧ + +record SymmetricMonoidalMonotone + {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} + (P : SymmetricMonoidalPreorder c₁ ℓ₁ e₁) + (Q : SymmetricMonoidalPreorder c₂ ℓ₂ e₂) + : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₁ ⊔ e₂) where + + private + module P = SymmetricMonoidalPreorder P + module Q = SymmetricMonoidalPreorder Q + + field + monoidalMonotone : MonoidalMonotone P.monoidalPreorder Q.monoidalPreorder + + open MonoidalMonotone monoidalMonotone public |