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 ------------------- 9 files changed, 406 insertions(+), 228 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 (limited to 'Category/Instance') 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} - } -- cgit v1.2.3