From 8ec259bb32b4339b27560f5ea13afa81b9b8febc Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 7 Jan 2026 10:12:13 -0600 Subject: Differentiate lax and strong monoidal monotones --- Category/Instance/MonoidalPreorders/Primitive.agda | 86 -------------------- .../Instance/Preorder/Primitive/Monoidals/Lax.agda | 87 ++++++++++++++++++++ .../Preorder/Primitive/Monoidals/Strong.agda | 92 ++++++++++++++++++++++ .../Primitive/Monoidals/Symmetric/Lax.agda | 84 ++++++++++++++++++++ .../Primitive/Monoidals/Symmetric/Strong.agda | 84 ++++++++++++++++++++ .../Instance/Preorder/Primitive/Preorders.agda | 58 ++++++++++++++ Category/Instance/Preorders.agda | 2 +- Category/Instance/Preorders/Primitive.agda | 58 -------------- Category/Instance/SymMonPre/Primitive.agda | 83 ------------------- Functor/Free/Instance/InducedSetoid.agda | 2 +- Functor/Free/Instance/MonoidalPreorder.agda | 75 ------------------ Functor/Free/Instance/MonoidalPreorder/Lax.agda | 76 ++++++++++++++++++ Functor/Free/Instance/Preorder.agda | 2 +- .../Free/Instance/SymmetricMonoidalPreorder.agda | 67 ---------------- .../Instance/SymmetricMonoidalPreorder/Lax.agda | 68 ++++++++++++++++ Preorder/Primitive/Monoidal.agda | 68 ++++------------ Preorder/Primitive/MonotoneMap/Monoidal/Lax.agda | 41 ++++++++++ .../Primitive/MonotoneMap/Monoidal/Strong.agda | 43 ++++++++++ 18 files changed, 652 insertions(+), 424 deletions(-) delete mode 100644 Category/Instance/MonoidalPreorders/Primitive.agda create mode 100644 Category/Instance/Preorder/Primitive/Monoidals/Lax.agda create mode 100644 Category/Instance/Preorder/Primitive/Monoidals/Strong.agda create mode 100644 Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda create mode 100644 Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Strong.agda create mode 100644 Category/Instance/Preorder/Primitive/Preorders.agda delete mode 100644 Category/Instance/Preorders/Primitive.agda delete mode 100644 Category/Instance/SymMonPre/Primitive.agda delete mode 100644 Functor/Free/Instance/MonoidalPreorder.agda create mode 100644 Functor/Free/Instance/MonoidalPreorder/Lax.agda delete mode 100644 Functor/Free/Instance/SymmetricMonoidalPreorder.agda create mode 100644 Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda create mode 100644 Preorder/Primitive/MonotoneMap/Monoidal/Lax.agda create mode 100644 Preorder/Primitive/MonotoneMap/Monoidal/Strong.agda diff --git a/Category/Instance/MonoidalPreorders/Primitive.agda b/Category/Instance/MonoidalPreorders/Primitive.agda deleted file mode 100644 index d00e17a..0000000 --- a/Category/Instance/MonoidalPreorders/Primitive.agda +++ /dev/null @@ -1,86 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Category.Instance.MonoidalPreorders.Primitive where - -import Preorder.Primitive.MonotoneMap as MonotoneMap using (_≃_; module ≃) - -open import Categories.Category using (Category) -open import Categories.Category.Helper using (categoryHelper) -open import Category.Instance.Preorders.Primitive using (Preorders) -open import Level using (Level; suc; _⊔_) -open import Preorder.Primitive.Monoidal using (MonoidalPreorder; MonoidalMonotone) -open import Relation.Binary using (IsEquivalence) - -module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : MonoidalPreorder c₁ ℓ₁} {B : MonoidalPreorder c₂ ℓ₂} where - - -- Pointwise equality of monoidal monotone maps - - open MonoidalMonotone using (F) - - _≃_ : (f g : MonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂) - f ≃ g = F f MonotoneMap.≃ F g - - infix 4 _≃_ - - ≃-isEquivalence : IsEquivalence _≃_ - ≃-isEquivalence = let open MonotoneMap.≃ in record - { refl = λ {x} → refl {x = F x} - ; sym = λ {f g} → sym {x = F f} {y = F g} - ; trans = λ {f g h} → trans {i = F f} {j = F g} {k = F h} - } - - module ≃ = IsEquivalence ≃-isEquivalence - -private - - identity : {c ℓ : Level} (A : MonoidalPreorder c ℓ) → MonoidalMonotone A A - identity A = let open MonoidalPreorder A in record - { F = Category.id (Preorders _ _) - ; ε = refl - ; ⊗-homo = λ p₁ p₂ → refl {p₁ ⊗ p₂} - } - - compose - : {c ℓ : Level} - {P Q R : MonoidalPreorder c ℓ} - → MonoidalMonotone Q R - → MonoidalMonotone P Q - → MonoidalMonotone P R - compose {R = R} G F = record - { F = let open Category (Preorders _ _) in G.F ∘ F.F - ; ε = trans G.ε (G.mono F.ε) - ; ⊗-homo = λ p₁ p₂ → trans (G.⊗-homo (F.map p₁) (F.map p₂)) (G.mono (F.⊗-homo p₁ p₂)) - } - where - module F = MonoidalMonotone F - module G = MonoidalMonotone G - open MonoidalPreorder R - - compose-resp-≃ - : {c ℓ : Level} - {A B C : MonoidalPreorder c ℓ} - {f h : MonoidalMonotone B C} - {g i : MonoidalMonotone A B} - → f ≃ h - → g ≃ i - → compose f g ≃ compose h i - compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = F f} {F g} {F h} {F i} - where - open Category (Preorders _ _) - open MonoidalMonotone using (F) - -MonoidalPreorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) -MonoidalPreorders c ℓ = categoryHelper record - { Obj = MonoidalPreorder c ℓ - ; _⇒_ = MonoidalMonotone - ; _≈_ = _≃_ - ; id = λ {A} → identity A - ; _∘_ = compose - ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} - ; identityˡ = λ {f = f} → ≃.refl {x = f} - ; identityʳ = λ {f = f} → ≃.refl {x = f} - ; equiv = ≃-isEquivalence - ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} - } - where - open MonoidalMonotone using (F) diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda b/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda new file mode 100644 index 0000000..cbd4015 --- /dev/null +++ b/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Instance.Preorder.Primitive.Monoidals.Lax where + +import Preorder.Primitive.MonotoneMap as MonotoneMap using (_≃_; module ≃) + +open import Categories.Category using (Category) +open import Categories.Category.Helper using (categoryHelper) +open import Category.Instance.Preorder.Primitive.Preorders using (Preorders) +open import Level using (Level; suc; _⊔_) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (MonoidalMonotone) +open import Relation.Binary using (IsEquivalence) + +module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : MonoidalPreorder c₁ ℓ₁} {B : MonoidalPreorder c₂ ℓ₂} where + + -- Pointwise equality of monoidal monotone maps + + open MonoidalMonotone using (F) + + _≃_ : (f g : MonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂) + f ≃ g = F f MonotoneMap.≃ F g + + infix 4 _≃_ + + ≃-isEquivalence : IsEquivalence _≃_ + ≃-isEquivalence = let open MonotoneMap.≃ in record + { refl = λ {x} → refl {x = F x} + ; sym = λ {f g} → sym {x = F f} {y = F g} + ; trans = λ {f g h} → trans {i = F f} {j = F g} {k = F h} + } + + module ≃ = IsEquivalence ≃-isEquivalence + +private + + identity : {c ℓ : Level} (A : MonoidalPreorder c ℓ) → MonoidalMonotone A A + identity A = let open MonoidalPreorder A in record + { F = Category.id (Preorders _ _) + ; ε = refl + ; ⊗-homo = λ p₁ p₂ → refl {p₁ ⊗ p₂} + } + + compose + : {c ℓ : Level} + {P Q R : MonoidalPreorder c ℓ} + → MonoidalMonotone Q R + → MonoidalMonotone P Q + → MonoidalMonotone P R + compose {R = R} G F = record + { F = let open Category (Preorders _ _) in G.F ∘ F.F + ; ε = trans G.ε (G.mono F.ε) + ; ⊗-homo = λ p₁ p₂ → trans (G.⊗-homo (F.map p₁) (F.map p₂)) (G.mono (F.⊗-homo p₁ p₂)) + } + where + module F = MonoidalMonotone F + module G = MonoidalMonotone G + open MonoidalPreorder R + + compose-resp-≃ + : {c ℓ : Level} + {A B C : MonoidalPreorder c ℓ} + {f h : MonoidalMonotone B C} + {g i : MonoidalMonotone A B} + → f ≃ h + → g ≃ i + → compose f g ≃ compose h i + compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = F f} {F g} {F h} {F i} + where + open Category (Preorders _ _) + open MonoidalMonotone using (F) + +Monoidals : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) +Monoidals c ℓ = categoryHelper record + { Obj = MonoidalPreorder c ℓ + ; _⇒_ = MonoidalMonotone + ; _≈_ = _≃_ + ; id = λ {A} → identity A + ; _∘_ = compose + ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} + ; identityˡ = λ {f = f} → ≃.refl {x = f} + ; identityʳ = λ {f = f} → ≃.refl {x = f} + ; equiv = ≃-isEquivalence + ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} + } + where + open MonoidalMonotone using (F) diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Strong.agda b/Category/Instance/Preorder/Primitive/Monoidals/Strong.agda new file mode 100644 index 0000000..470db1c --- /dev/null +++ b/Category/Instance/Preorder/Primitive/Monoidals/Strong.agda @@ -0,0 +1,92 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Instance.Preorder.Primitive.Monoidals.Strong where + +import Preorder.Primitive.MonotoneMap as MonotoneMap using (_≃_; module ≃) + +open import Categories.Category using (Category) +open import Categories.Category.Helper using (categoryHelper) +open import Category.Instance.Preorder.Primitive.Preorders using (Preorders) +open import Level using (Level; suc; _⊔_) +open import Preorder.Primitive using (module Isomorphism) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (MonoidalMonotone) +open import Relation.Binary using (IsEquivalence) + +module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : MonoidalPreorder c₁ ℓ₁} {B : MonoidalPreorder c₂ ℓ₂} where + + -- Pointwise equality of monoidal monotone maps + + open MonoidalMonotone using (F) + + _≃_ : (f g : MonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂) + f ≃ g = F f MonotoneMap.≃ F g + + infix 4 _≃_ + + ≃-isEquivalence : IsEquivalence _≃_ + ≃-isEquivalence = let open MonotoneMap.≃ in record + { refl = λ {x} → refl {x = F x} + ; sym = λ {f g} → sym {x = F f} {y = F g} + ; trans = λ {f g h} → trans {i = F f} {j = F g} {k = F h} + } + + module ≃ = IsEquivalence ≃-isEquivalence + +private + + identity : {c ℓ : Level} (A : MonoidalPreorder c ℓ) → MonoidalMonotone A A + identity A = record + { F = Category.id (Preorders _ _) + ; ε = ≅.refl + ; ⊗-homo = λ p₁ p₂ → ≅.refl {p₁ ⊗ p₂} + } + where + open MonoidalPreorder A + open Isomorphism U using (module ≅) + + compose + : {c ℓ : Level} + {P Q R : MonoidalPreorder c ℓ} + → MonoidalMonotone Q R + → MonoidalMonotone P Q + → MonoidalMonotone P R + compose {R = R} G F = record + { F = let open Category (Preorders _ _) in G.F ∘ F.F + ; ε = ≅.trans G.ε (G.map-resp-≅ F.ε) + ; ⊗-homo = λ p₁ p₂ → ≅.trans (G.⊗-homo (F.map p₁) (F.map p₂)) (G.map-resp-≅ (F.⊗-homo p₁ p₂)) + } + where + module F = MonoidalMonotone F + module G = MonoidalMonotone G + open MonoidalPreorder R + open Isomorphism U using (module ≅) + + compose-resp-≃ + : {c ℓ : Level} + {A B C : MonoidalPreorder c ℓ} + {f h : MonoidalMonotone B C} + {g i : MonoidalMonotone A B} + → f ≃ h + → g ≃ i + → compose f g ≃ compose h i + compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = F f} {F g} {F h} {F i} + where + open Category (Preorders _ _) + open MonoidalMonotone using (F) + +Monoidals : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) +Monoidals c ℓ = categoryHelper record + { Obj = MonoidalPreorder c ℓ + ; _⇒_ = MonoidalMonotone + ; _≈_ = _≃_ + ; id = λ {A} → identity A + ; _∘_ = compose + ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} + ; identityˡ = λ {f = f} → ≃.refl {x = f} + ; identityʳ = λ {f = f} → ≃.refl {x = f} + ; equiv = ≃-isEquivalence + ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} + } + where + open MonoidalMonotone using (F) diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda new file mode 100644 index 0000000..c15ff29 --- /dev/null +++ b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda @@ -0,0 +1,84 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Lax where + +import Category.Instance.Preorder.Primitive.Monoidals.Lax as MP using (_≃_; module ≃) + +open import Categories.Category using (Category) +open import Categories.Category.Helper using (categoryHelper) +open import Category.Instance.Preorder.Primitive.Monoidals.Lax using (Monoidals) +open import Level using (Level; suc; _⊔_) +open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (SymmetricMonoidalMonotone) +open import Relation.Binary using (IsEquivalence) + +module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : SymmetricMonoidalPreorder c₁ ℓ₁} {B : SymmetricMonoidalPreorder c₂ ℓ₂} where + + open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) + + -- Pointwise isomorphism 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 + +private + + identity : {c ℓ : Level} (A : SymmetricMonoidalPreorder c ℓ) → SymmetricMonoidalMonotone A A + identity {c} {ℓ} A = record + { monoidalMonotone = id {monoidalPreorder} + } + where + open SymmetricMonoidalPreorder A using (monoidalPreorder) + open Category (Monoidals c ℓ) using (id) + + compose + : {c ℓ : Level} + {P Q R : SymmetricMonoidalPreorder c ℓ} + → SymmetricMonoidalMonotone Q R + → SymmetricMonoidalMonotone P Q + → SymmetricMonoidalMonotone P R + compose {c} {ℓ} {R = R} G F = record + { monoidalMonotone = G.monoidalMonotone ∘ F.monoidalMonotone + } + where + module G = SymmetricMonoidalMonotone G + module F = SymmetricMonoidalMonotone F + open Category (Monoidals c ℓ) using (_∘_) + + compose-resp-≃ + : {c ℓ : Level} + {A B C : SymmetricMonoidalPreorder c ℓ} + {f h : SymmetricMonoidalMonotone B C} + {g i : SymmetricMonoidalMonotone A B} + → f ≃ h + → g ≃ i + → compose f g ≃ compose h i + compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = mM f} {mM g} {mM h} {mM i} + where + open Category (Monoidals _ _) + open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) + +-- The category of symmetric monoidal preorders and lax symmetric monoidal monotone +SymMonPre : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) +SymMonPre c ℓ = categoryHelper record + { Obj = SymmetricMonoidalPreorder c ℓ + ; _⇒_ = SymmetricMonoidalMonotone + ; _≈_ = _≃_ + ; id = λ {A} → identity A + ; _∘_ = compose + ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} + ; identityˡ = λ {f = f} → ≃.refl {x = f} + ; identityʳ = λ {f = f} → ≃.refl {x = f} + ; equiv = ≃-isEquivalence + ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} + } diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Strong.agda b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Strong.agda new file mode 100644 index 0000000..b584ed7 --- /dev/null +++ b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Strong.agda @@ -0,0 +1,84 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Strong where + +import Category.Instance.Preorder.Primitive.Monoidals.Strong as MP using (_≃_; module ≃) + +open import Categories.Category using (Category) +open import Categories.Category.Helper using (categoryHelper) +open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (Monoidals) +open import Level using (Level; suc; _⊔_) +open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (SymmetricMonoidalMonotone) +open import Relation.Binary using (IsEquivalence) + +module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : SymmetricMonoidalPreorder c₁ ℓ₁} {B : SymmetricMonoidalPreorder c₂ ℓ₂} where + + open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) + + -- Pointwise isomorphism 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 + +private + + identity : {c ℓ : Level} (A : SymmetricMonoidalPreorder c ℓ) → SymmetricMonoidalMonotone A A + identity {c} {ℓ} A = record + { monoidalMonotone = id {monoidalPreorder} + } + where + open SymmetricMonoidalPreorder A using (monoidalPreorder) + open Category (Monoidals c ℓ) using (id) + + compose + : {c ℓ : Level} + {P Q R : SymmetricMonoidalPreorder c ℓ} + → SymmetricMonoidalMonotone Q R + → SymmetricMonoidalMonotone P Q + → SymmetricMonoidalMonotone P R + compose {c} {ℓ} {R = R} G F = record + { monoidalMonotone = G.monoidalMonotone ∘ F.monoidalMonotone + } + where + module G = SymmetricMonoidalMonotone G + module F = SymmetricMonoidalMonotone F + open Category (Monoidals c ℓ) using (_∘_) + + compose-resp-≃ + : {c ℓ : Level} + {A B C : SymmetricMonoidalPreorder c ℓ} + {f h : SymmetricMonoidalMonotone B C} + {g i : SymmetricMonoidalMonotone A B} + → f ≃ h + → g ≃ i + → compose f g ≃ compose h i + compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = mM f} {mM g} {mM h} {mM i} + where + open Category (Monoidals _ _) + open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) + +-- The category of symmetric monoidal preorders and strong symmetric monoidal monotone +SymMonPre : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) +SymMonPre c ℓ = categoryHelper record + { Obj = SymmetricMonoidalPreorder c ℓ + ; _⇒_ = SymmetricMonoidalMonotone + ; _≈_ = _≃_ + ; id = λ {A} → identity A + ; _∘_ = compose + ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} + ; identityˡ = λ {f = f} → ≃.refl {x = f} + ; identityʳ = λ {f = f} → ≃.refl {x = f} + ; equiv = ≃-isEquivalence + ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} + } diff --git a/Category/Instance/Preorder/Primitive/Preorders.agda b/Category/Instance/Preorder/Primitive/Preorders.agda new file mode 100644 index 0000000..9832376 --- /dev/null +++ b/Category/Instance/Preorder/Primitive/Preorders.agda @@ -0,0 +1,58 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Instance.Preorder.Primitive.Preorders where + +open import Categories.Category using (Category) +open import Categories.Category.Helper using (categoryHelper) +open import Function using (id; _∘_) +open import Level using (Level; _⊔_; suc) +open import Preorder.Primitive using (Preorder; module Isomorphism) +open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃) + +-- The category of primitive preorders and monotone maps + +private + + module _ {c ℓ : Level} where + + identity : {A : Preorder c ℓ} → MonotoneMap A A + identity = record + { map = id + ; mono = id + } + + compose : {A B C : Preorder c ℓ} → MonotoneMap B C → MonotoneMap A B → MonotoneMap A C + compose f g = record + { map = f.map ∘ g.map + ; mono = f.mono ∘ g.mono + } + where + module f = MonotoneMap f + module g = MonotoneMap g + + compose-resp-≃ + : {A B C : Preorder c ℓ} + {f h : MonotoneMap B C} + {g i : MonotoneMap A B} + → f ≃ h + → g ≃ i + → compose f g ≃ compose h i + compose-resp-≃ {C = C} {h = h} {g} f≃h g≃i x = ≅.trans (f≃h (map g x)) (map-resp-≅ h (g≃i x)) + where + open MonotoneMap using (map; mono; map-resp-≅) + open Preorder C + open Isomorphism C + +Preorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) +Preorders c ℓ = categoryHelper record + { Obj = Preorder c ℓ + ; _⇒_ = MonotoneMap + ; _≈_ = _≃_ + ; id = identity + ; _∘_ = compose + ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} + ; identityˡ = λ {f = f} → ≃.refl {x = f} + ; identityʳ = λ {f = f} → ≃.refl {x = f} + ; equiv = ≃-isEquivalence + ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} + } diff --git a/Category/Instance/Preorders.agda b/Category/Instance/Preorders.agda index 6d69eda..1a663ac 100644 --- a/Category/Instance/Preorders.agda +++ b/Category/Instance/Preorders.agda @@ -31,7 +31,7 @@ module _ {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} {A : Preorder c₁ ℓ₁ e module ≗ = IsEquivalence ≗-isEquivalence --- The category of preorders and monotone maps +-- The category of preorders and preorder homomorphisms Preorders : (c ℓ e : Level) → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ) Preorders c ℓ e = record diff --git a/Category/Instance/Preorders/Primitive.agda b/Category/Instance/Preorders/Primitive.agda deleted file mode 100644 index 9c36d03..0000000 --- a/Category/Instance/Preorders/Primitive.agda +++ /dev/null @@ -1,58 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Category.Instance.Preorders.Primitive where - -open import Categories.Category using (Category) -open import Categories.Category.Helper using (categoryHelper) -open import Function using (id; _∘_) -open import Level using (Level; _⊔_; suc) -open import Preorder.Primitive using (Preorder; module Isomorphism) -open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃) - --- The category of primitive preorders and monotone maps - -private - - module _ {c ℓ : Level} where - - identity : {A : Preorder c ℓ} → MonotoneMap A A - identity = record - { map = id - ; mono = id - } - - compose : {A B C : Preorder c ℓ} → MonotoneMap B C → MonotoneMap A B → MonotoneMap A C - compose f g = record - { map = f.map ∘ g.map - ; mono = f.mono ∘ g.mono - } - where - module f = MonotoneMap f - module g = MonotoneMap g - - compose-resp-≃ - : {A B C : Preorder c ℓ} - {f h : MonotoneMap B C} - {g i : MonotoneMap A B} - → f ≃ h - → g ≃ i - → compose f g ≃ compose h i - compose-resp-≃ {C = C} {h = h} {g} f≃h g≃i x = ≅.trans (f≃h (map g x)) (map-resp-≅ h (g≃i x)) - where - open MonotoneMap using (map; mono; map-resp-≅) - open Preorder C - open Isomorphism C - -Preorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) -Preorders c ℓ = categoryHelper record - { Obj = Preorder c ℓ - ; _⇒_ = MonotoneMap - ; _≈_ = _≃_ - ; id = identity - ; _∘_ = compose - ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} - ; identityˡ = λ {f = f} → ≃.refl {x = f} - ; identityʳ = λ {f = f} → ≃.refl {x = f} - ; equiv = ≃-isEquivalence - ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} - } diff --git a/Category/Instance/SymMonPre/Primitive.agda b/Category/Instance/SymMonPre/Primitive.agda deleted file mode 100644 index 7475719..0000000 --- a/Category/Instance/SymMonPre/Primitive.agda +++ /dev/null @@ -1,83 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Category.Instance.SymMonPre.Primitive where - -import Category.Instance.MonoidalPreorders.Primitive as MP using (_≃_; module ≃) - -open import Categories.Category using (Category) -open import Categories.Category.Helper using (categoryHelper) -open import Category.Instance.MonoidalPreorders.Primitive using (MonoidalPreorders) -open import Level using (Level; suc; _⊔_) -open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder; SymmetricMonoidalMonotone) -open import Relation.Binary using (IsEquivalence) - -module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : SymmetricMonoidalPreorder c₁ ℓ₁} {B : SymmetricMonoidalPreorder c₂ ℓ₂} where - - open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) - - -- Pointwise isomorphism 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 - -private - - identity : {c ℓ : Level} (A : SymmetricMonoidalPreorder c ℓ) → SymmetricMonoidalMonotone A A - identity {c} {ℓ} A = record - { monoidalMonotone = id {monoidalPreorder} - } - where - open SymmetricMonoidalPreorder A using (monoidalPreorder) - open Category (MonoidalPreorders c ℓ) using (id) - - compose - : {c ℓ : Level} - {P Q R : SymmetricMonoidalPreorder c ℓ} - → SymmetricMonoidalMonotone Q R - → SymmetricMonoidalMonotone P Q - → SymmetricMonoidalMonotone P R - compose {c} {ℓ} {R = R} G F = record - { monoidalMonotone = G.monoidalMonotone ∘ F.monoidalMonotone - } - where - module G = SymmetricMonoidalMonotone G - module F = SymmetricMonoidalMonotone F - open Category (MonoidalPreorders c ℓ) using (_∘_) - - compose-resp-≃ - : {c ℓ : Level} - {A B C : SymmetricMonoidalPreorder c ℓ} - {f h : SymmetricMonoidalMonotone B C} - {g i : SymmetricMonoidalMonotone A B} - → f ≃ h - → g ≃ i - → compose f g ≃ compose h i - compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = mM f} {mM g} {mM h} {mM i} - where - open Category (MonoidalPreorders _ _) - open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) - --- The category of symmetric monoidal preorders -SymMonPre : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) -SymMonPre c ℓ = categoryHelper record - { Obj = SymmetricMonoidalPreorder c ℓ - ; _⇒_ = SymmetricMonoidalMonotone - ; _≈_ = _≃_ - ; id = λ {A} → identity A - ; _∘_ = compose - ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f} - ; identityˡ = λ {f = f} → ≃.refl {x = f} - ; identityʳ = λ {f = f} → ≃.refl {x = f} - ; equiv = ≃-isEquivalence - ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i} - } diff --git a/Functor/Free/Instance/InducedSetoid.agda b/Functor/Free/Instance/InducedSetoid.agda index 08b65e3..83aaedf 100644 --- a/Functor/Free/Instance/InducedSetoid.agda +++ b/Functor/Free/Instance/InducedSetoid.agda @@ -6,7 +6,7 @@ module Functor.Free.Instance.InducedSetoid where open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) -open import Category.Instance.Preorders.Primitive using (Preorders) +open import Category.Instance.Preorder.Primitive.Preorders using (Preorders) open import Function using (Func) open import Level using (Level) open import Preorder.Primitive using (Preorder; module Isomorphism) diff --git a/Functor/Free/Instance/MonoidalPreorder.agda b/Functor/Free/Instance/MonoidalPreorder.agda deleted file mode 100644 index ca03786..0000000 --- a/Functor/Free/Instance/MonoidalPreorder.agda +++ /dev/null @@ -1,75 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Functor.Free.Instance.MonoidalPreorder where - -import Categories.Category.Monoidal.Utilities as ⊗-Util - -open import Categories.Category using (Category) -open import Categories.Category.Instance.Monoidals using (Monoidals) -open import Categories.Category.Monoidal using (MonoidalCategory) -open import Categories.Functor using (Functor) -open import Categories.Functor.Monoidal using (MonoidalFunctor) -open import Categories.Functor.Monoidal.Properties using (∘-Monoidal) -open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using (module Lax) -open import Category.Instance.MonoidalPreorders.Primitive using (MonoidalPreorders; _≃_; module ≃) -open import Data.Product using (_,_) -open import Level using (Level) -open import Preorder.Primitive.Monoidal using (MonoidalPreorder; MonoidalMonotone) - -open Lax using (MonoidalNaturalIsomorphism) -  --- The free monoidal preorder of a monoidal category - -import Functor.Free.Instance.Preorder as Preorder - -module _ {o ℓ e : Level} where - - monoidalPreorder : MonoidalCategory o ℓ e → MonoidalPreorder o ℓ - monoidalPreorder C = record - { U = Preorder.Free.₀ U - ; monoidal = record - { unit = unit - ; tensor = Preorder.Free.₁ ⊗ - ; unitaryˡ = Preorder.Free.F-resp-≈ unitorˡ-naturalIsomorphism - ; unitaryʳ = Preorder.Free.F-resp-≈ unitorʳ-naturalIsomorphism - ; associative = λ x y z → record - { from = associator.from {x} {y} {z} - ; to = associator.to {x} {y} {z} - } - } - } - where - open MonoidalCategory C - open ⊗-Util monoidal - - module _ {A B : MonoidalCategory o ℓ e} where - - monoidalMonotone : MonoidalFunctor A B → MonoidalMonotone (monoidalPreorder A) (monoidalPreorder B) - monoidalMonotone F = record - { F = Preorder.Free.₁ F.F - ; ε = F.ε - ; ⊗-homo = λ p₁ p₂ → F.⊗-homo.η (p₁ , p₂) - } - where - module F = MonoidalFunctor F - - open MonoidalNaturalIsomorphism using (U) - - pointwiseIsomorphism - : {F G : MonoidalFunctor A B} - → MonoidalNaturalIsomorphism F G - → monoidalMonotone F ≃ monoidalMonotone G - pointwiseIsomorphism F≃G = Preorder.Free.F-resp-≈ (U F≃G) - -Free : {o ℓ e : Level} → Functor (Monoidals o ℓ e) (MonoidalPreorders o ℓ) -Free = record - { F₀ = monoidalPreorder - ; F₁ = monoidalMonotone - ; identity = λ {A} → ≃.refl {A = monoidalPreorder A} {x = id} - ; homomorphism = λ {f = f} {h} → ≃.refl {x = monoidalMonotone (∘-Monoidal h f)} - ; F-resp-≈ = pointwiseIsomorphism - } - where - open Category (MonoidalPreorders _ _) using (id) - -module Free {o ℓ e} = Functor (Free {o} {ℓ} {e}) diff --git a/Functor/Free/Instance/MonoidalPreorder/Lax.agda b/Functor/Free/Instance/MonoidalPreorder/Lax.agda new file mode 100644 index 0000000..be4e835 --- /dev/null +++ b/Functor/Free/Instance/MonoidalPreorder/Lax.agda @@ -0,0 +1,76 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Free.Instance.MonoidalPreorder.Lax where + +import Categories.Category.Monoidal.Utilities as ⊗-Util + +open import Categories.Category using (Category) +open import Categories.Category.Instance.Monoidals using (Monoidals) +open import Categories.Category.Monoidal using (MonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.Functor.Monoidal using (MonoidalFunctor) +open import Categories.Functor.Monoidal.Properties using (∘-Monoidal) +open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using (module Lax) +open import Category.Instance.Preorder.Primitive.Monoidals.Lax using (_≃_; module ≃) renaming (Monoidals to Monoidalsₚ) +open import Data.Product using (_,_) +open import Level using (Level) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (MonoidalMonotone) + +open Lax using (MonoidalNaturalIsomorphism) +  +-- The free monoidal preorder of a monoidal category + +import Functor.Free.Instance.Preorder as Preorder + +module _ {o ℓ e : Level} where + + monoidalPreorder : MonoidalCategory o ℓ e → MonoidalPreorder o ℓ + monoidalPreorder C = record + { U = Preorder.Free.₀ U + ; monoidal = record + { unit = unit + ; tensor = Preorder.Free.₁ ⊗ + ; unitaryˡ = Preorder.Free.F-resp-≈ unitorˡ-naturalIsomorphism + ; unitaryʳ = Preorder.Free.F-resp-≈ unitorʳ-naturalIsomorphism + ; associative = λ x y z → record + { from = associator.from {x} {y} {z} + ; to = associator.to {x} {y} {z} + } + } + } + where + open MonoidalCategory C + open ⊗-Util monoidal + + module _ {A B : MonoidalCategory o ℓ e} where + + monoidalMonotone : MonoidalFunctor A B → MonoidalMonotone (monoidalPreorder A) (monoidalPreorder B) + monoidalMonotone F = record + { F = Preorder.Free.₁ F.F + ; ε = F.ε + ; ⊗-homo = λ p₁ p₂ → F.⊗-homo.η (p₁ , p₂) + } + where + module F = MonoidalFunctor F + + open MonoidalNaturalIsomorphism using (U) + + pointwiseIsomorphism + : {F G : MonoidalFunctor A B} + → MonoidalNaturalIsomorphism F G + → monoidalMonotone F ≃ monoidalMonotone G + pointwiseIsomorphism F≃G = Preorder.Free.F-resp-≈ (U F≃G) + +Free : {o ℓ e : Level} → Functor (Monoidals o ℓ e) (Monoidalsₚ o ℓ) +Free = record + { F₀ = monoidalPreorder + ; F₁ = monoidalMonotone + ; identity = λ {A} → ≃.refl {A = monoidalPreorder A} {x = id} + ; homomorphism = λ {f = f} {h} → ≃.refl {x = monoidalMonotone (∘-Monoidal h f)} + ; F-resp-≈ = pointwiseIsomorphism + } + where + open Category (Monoidalsₚ _ _) using (id) + +module Free {o ℓ e} = Functor (Free {o} {ℓ} {e}) diff --git a/Functor/Free/Instance/Preorder.agda b/Functor/Free/Instance/Preorder.agda index 27be24e..18583e9 100644 --- a/Functor/Free/Instance/Preorder.agda +++ b/Functor/Free/Instance/Preorder.agda @@ -7,7 +7,7 @@ open import Categories.Category.Instance.Cats using (Cats) open import Function using (flip) open import Categories.Functor using (Functor; _∘F_) open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism) -open import Category.Instance.Preorders.Primitive using (Preorders) +open import Category.Instance.Preorder.Primitive.Preorders using (Preorders) open import Level using (Level; _⊔_; suc) open import Preorder.Primitive using (Preorder; module Isomorphism) open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; module ≃) diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder.agda deleted file mode 100644 index 2fcecce..0000000 --- a/Functor/Free/Instance/SymmetricMonoidalPreorder.agda +++ /dev/null @@ -1,67 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Functor.Free.Instance.SymmetricMonoidalPreorder where - -import Functor.Free.Instance.MonoidalPreorder as MP - -open import Categories.Category using (Category) -open import Category.Instance.SymMonCat using (SymMonCat) -open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) -open import Categories.Functor using (Functor) -open import Categories.Functor.Monoidal.Symmetric using () renaming (module Lax to Lax₁) -open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-SymmetricMonoidal) -open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Lax to Lax₂) -open import Category.Instance.SymMonPre.Primitive using (SymMonPre; _≃_; module ≃) -open import Data.Product using (_,_) -open import Level using (Level) -open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder; SymmetricMonoidalMonotone) - -open Lax₁ using (SymmetricMonoidalFunctor) -open Lax₂ using (SymmetricMonoidalNaturalIsomorphism) -  --- The free symmetric monoidal preorder of a symmetric monoidal category - -module _ {o ℓ e : Level} where - - symmetricMonoidalPreorder : SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalPreorder o ℓ - symmetricMonoidalPreorder C = record - { M - ; symmetric = record - { symmetric = λ x y → braiding.⇒.η (x , y) - } - } - where - open SymmetricMonoidalCategory C - module M = MonoidalPreorder (MP.Free.₀ monoidalCategory) - - module _ {A B : SymmetricMonoidalCategory o ℓ e} where - - symmetricMonoidalMonotone - : SymmetricMonoidalFunctor A B - → SymmetricMonoidalMonotone (symmetricMonoidalPreorder A) (symmetricMonoidalPreorder B) - symmetricMonoidalMonotone F = record - { monoidalMonotone = MP.Free.₁ F.monoidalFunctor - } - where - module F = SymmetricMonoidalFunctor F - - open SymmetricMonoidalNaturalIsomorphism using (⌊_⌋) - - pointwiseIsomorphism - : {F G : SymmetricMonoidalFunctor A B} - → SymmetricMonoidalNaturalIsomorphism F G - → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G - pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋ - -Free : {o ℓ e : Level} → Functor (SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) -Free = record - { F₀ = symmetricMonoidalPreorder - ; F₁ = symmetricMonoidalMonotone - ; identity = λ {A} → ≃.refl {A = symmetricMonoidalPreorder A} {x = id} - ; homomorphism = λ {f = f} {h} → ≃.refl {x = symmetricMonoidalMonotone (∘-SymmetricMonoidal h f)} - ; F-resp-≈ = pointwiseIsomorphism - } - where - open Category (SymMonPre _ _) using (id) - -module Free {o ℓ e} = Functor (Free {o} {ℓ} {e}) diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda new file mode 100644 index 0000000..8bf567d --- /dev/null +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda @@ -0,0 +1,68 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Free.Instance.SymmetricMonoidalPreorder.Lax where + +import Functor.Free.Instance.MonoidalPreorder.Lax as MP + +open import Categories.Category using (Category) +open import Category.Instance.SymMonCat using (SymMonCat) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.Functor.Monoidal.Symmetric using () renaming (module Lax to Lax₁) +open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-SymmetricMonoidal) +open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Lax to Lax₂) +open import Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Lax using (SymMonPre; _≃_; module ≃) +open import Data.Product using (_,_) +open import Level using (Level) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (SymmetricMonoidalMonotone) + +open Lax₁ using (SymmetricMonoidalFunctor) +open Lax₂ using (SymmetricMonoidalNaturalIsomorphism) +  +-- The free symmetric monoidal preorder of a symmetric monoidal category + +module _ {o ℓ e : Level} where + + symmetricMonoidalPreorder : SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalPreorder o ℓ + symmetricMonoidalPreorder C = record + { M + ; symmetric = record + { symmetric = λ x y → braiding.⇒.η (x , y) + } + } + where + open SymmetricMonoidalCategory C + module M = MonoidalPreorder (MP.Free.₀ monoidalCategory) + + module _ {A B : SymmetricMonoidalCategory o ℓ e} where + + symmetricMonoidalMonotone + : SymmetricMonoidalFunctor A B + → SymmetricMonoidalMonotone (symmetricMonoidalPreorder A) (symmetricMonoidalPreorder B) + symmetricMonoidalMonotone F = record + { monoidalMonotone = MP.Free.₁ F.monoidalFunctor + } + where + module F = SymmetricMonoidalFunctor F + + open SymmetricMonoidalNaturalIsomorphism using (⌊_⌋) + + pointwiseIsomorphism + : {F G : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism F G + → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G + pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋ + +Free : {o ℓ e : Level} → Functor (SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) +Free = record + { F₀ = symmetricMonoidalPreorder + ; F₁ = symmetricMonoidalMonotone + ; identity = λ {A} → ≃.refl {A = symmetricMonoidalPreorder A} {x = id} + ; homomorphism = λ {f = f} {h} → ≃.refl {x = symmetricMonoidalMonotone (∘-SymmetricMonoidal h f)} + ; F-resp-≈ = pointwiseIsomorphism + } + where + open Category (SymMonPre _ _) using (id) + +module Free {o ℓ e} = Functor (Free {o} {ℓ} {e}) diff --git a/Preorder/Primitive/Monoidal.agda b/Preorder/Primitive/Monoidal.agda index b000d32..af57b70 100644 --- a/Preorder/Primitive/Monoidal.agda +++ b/Preorder/Primitive/Monoidal.agda @@ -8,24 +8,22 @@ open import Preorder.Primitive.MonotoneMap using (MonotoneMap) open import Data.Product using (_×_; _,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise; ×-refl; ×-transitive) -private - - _×ₚ_ - : {c₁ c₂ ℓ₁ ℓ₂ : Level} - → Preorder c₁ ℓ₁ - → Preorder c₂ ℓ₂ - → Preorder (c₁ ⊔ c₂) (ℓ₁ ⊔ ℓ₂) - _×ₚ_ P Q = record - { Carrier = P.Carrier × Q.Carrier - ; _≲_ = Pointwise P._≲_ Q._≲_ - ; refl = ×-refl {R = P._≲_} {S = Q._≲_} P.refl Q.refl - ; trans = ×-transitive {R = P._≲_} {S = Q._≲_} P.trans Q.trans - } - where - module P = Preorder P - module Q = Preorder Q - - infixr 2 _×ₚ_ +_×ₚ_ + : {c₁ c₂ ℓ₁ ℓ₂ : Level} + → Preorder c₁ ℓ₁ + → Preorder c₂ ℓ₂ + → Preorder (c₁ ⊔ c₂) (ℓ₁ ⊔ ℓ₂) +_×ₚ_ P Q = record + { Carrier = P.Carrier × Q.Carrier + ; _≲_ = Pointwise P._≲_ Q._≲_ + ; refl = ×-refl {R = P._≲_} {S = Q._≲_} P.refl Q.refl + ; trans = ×-transitive {R = P._≲_} {S = Q._≲_} P.trans Q.trans + } + where + module P = Preorder P + module Q = Preorder Q + +infixr 2 _×ₚ_ record Monoidal {c ℓ : Level} (P : Preorder c ℓ) : Set (c ⊔ ℓ) where @@ -78,37 +76,3 @@ record SymmetricMonoidalPreorder (c ℓ : Level) : Set (suc (c ⊔ ℓ)) where open Preorder U public open Monoidal monoidal public open Symmetric symmetric public - -record MonoidalMonotone - {c₁ c₂ ℓ₁ ℓ₂ : Level} - (P : MonoidalPreorder c₁ ℓ₁) - (Q : MonoidalPreorder c₂ ℓ₂) - : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where - - private - module P = MonoidalPreorder P - module Q = MonoidalPreorder Q - - field - F : MonotoneMap P.U Q.U - - open MonotoneMap F public - - field - ε : Q.unit Q.≲ map P.unit - ⊗-homo : (p₁ p₂ : P.Carrier) → map p₁ Q.⊗ map p₂ Q.≲ map (p₁ P.⊗ p₂) - -record SymmetricMonoidalMonotone - {c₁ c₂ ℓ₁ ℓ₂ : Level} - (P : SymmetricMonoidalPreorder c₁ ℓ₁) - (Q : SymmetricMonoidalPreorder c₂ ℓ₂) - : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where - - private - module P = SymmetricMonoidalPreorder P - module Q = SymmetricMonoidalPreorder Q - - field - monoidalMonotone : MonoidalMonotone P.monoidalPreorder Q.monoidalPreorder - - open MonoidalMonotone monoidalMonotone public diff --git a/Preorder/Primitive/MonotoneMap/Monoidal/Lax.agda b/Preorder/Primitive/MonotoneMap/Monoidal/Lax.agda new file mode 100644 index 0000000..703f3be --- /dev/null +++ b/Preorder/Primitive/MonotoneMap/Monoidal/Lax.agda @@ -0,0 +1,41 @@ +{-# OPTIONS --without-K --safe #-} + +module Preorder.Primitive.MonotoneMap.Monoidal.Lax where + +open import Level using (Level; _⊔_) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder) +open import Preorder.Primitive.MonotoneMap using (MonotoneMap) + +record MonoidalMonotone + {c₁ c₂ ℓ₁ ℓ₂ : Level} + (P : MonoidalPreorder c₁ ℓ₁) + (Q : MonoidalPreorder c₂ ℓ₂) + : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where + + private + module P = MonoidalPreorder P + module Q = MonoidalPreorder Q + + field + F : MonotoneMap P.U Q.U + + open MonotoneMap F public + + field + ε : Q.unit Q.≲ map P.unit + ⊗-homo : (p₁ p₂ : P.Carrier) → map p₁ Q.⊗ map p₂ Q.≲ map (p₁ P.⊗ p₂) + +record SymmetricMonoidalMonotone + {c₁ c₂ ℓ₁ ℓ₂ : Level} + (P : SymmetricMonoidalPreorder c₁ ℓ₁) + (Q : SymmetricMonoidalPreorder c₂ ℓ₂) + : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where + + private + module P = SymmetricMonoidalPreorder P + module Q = SymmetricMonoidalPreorder Q + + field + monoidalMonotone : MonoidalMonotone P.monoidalPreorder Q.monoidalPreorder + + open MonoidalMonotone monoidalMonotone public diff --git a/Preorder/Primitive/MonotoneMap/Monoidal/Strong.agda b/Preorder/Primitive/MonotoneMap/Monoidal/Strong.agda new file mode 100644 index 0000000..f613b14 --- /dev/null +++ b/Preorder/Primitive/MonotoneMap/Monoidal/Strong.agda @@ -0,0 +1,43 @@ +{-# OPTIONS --without-K --safe #-} + +module Preorder.Primitive.MonotoneMap.Monoidal.Strong where + +open import Level using (Level; _⊔_) +open import Preorder.Primitive using (module Isomorphism) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder) +open import Preorder.Primitive.MonotoneMap using (MonotoneMap) + +record MonoidalMonotone + {c₁ c₂ ℓ₁ ℓ₂ : Level} + (P : MonoidalPreorder c₁ ℓ₁) + (Q : MonoidalPreorder c₂ ℓ₂) + : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where + + private + module P = MonoidalPreorder P + module Q = MonoidalPreorder Q + + field + F : MonotoneMap P.U Q.U + + open MonotoneMap F public + open Isomorphism Q.U using (_≅_) + + field + ε : Q.unit ≅ map P.unit + ⊗-homo : (p₁ p₂ : P.Carrier) → map p₁ Q.⊗ map p₂ ≅ map (p₁ P.⊗ p₂) + +record SymmetricMonoidalMonotone + {c₁ c₂ ℓ₁ ℓ₂ : Level} + (P : SymmetricMonoidalPreorder c₁ ℓ₁) + (Q : SymmetricMonoidalPreorder c₂ ℓ₂) + : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where + + private + module P = SymmetricMonoidalPreorder P + module Q = SymmetricMonoidalPreorder Q + + field + monoidalMonotone : MonoidalMonotone P.monoidalPreorder Q.monoidalPreorder + + open MonoidalMonotone monoidalMonotone public -- cgit v1.2.3