diff options
13 files changed, 306 insertions, 78 deletions
diff --git a/Category/Instance/MonoidalPreorders/Primitive.agda b/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda index d00e17a..cbd4015 100644 --- a/Category/Instance/MonoidalPreorders/Primitive.agda +++ b/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda @@ -1,14 +1,15 @@ {-# OPTIONS --without-K --safe #-} -module Category.Instance.MonoidalPreorders.Primitive where +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.Preorders.Primitive using (Preorders) +open import Category.Instance.Preorder.Primitive.Preorders using (Preorders) open import Level using (Level; suc; _⊔_) -open import Preorder.Primitive.Monoidal using (MonoidalPreorder; MonoidalMonotone) +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 @@ -69,8 +70,8 @@ private open Category (Preorders _ _) open MonoidalMonotone using (F) -MonoidalPreorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) -MonoidalPreorders c ℓ = categoryHelper record +Monoidals : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) +Monoidals c ℓ = categoryHelper record { Obj = MonoidalPreorder c ℓ ; _⇒_ = MonoidalMonotone ; _≈_ = _≃_ 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/SymMonPre/Primitive.agda b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda index 7475719..c15ff29 100644 --- a/Category/Instance/SymMonPre/Primitive.agda +++ b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda @@ -1,14 +1,15 @@ {-# OPTIONS --without-K --safe #-} -module Category.Instance.SymMonPre.Primitive where +module Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Lax where -import Category.Instance.MonoidalPreorders.Primitive as MP using (_≃_; module ≃) +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.MonoidalPreorders.Primitive using (MonoidalPreorders) +open import Category.Instance.Preorder.Primitive.Monoidals.Lax using (Monoidals) open import Level using (Level; suc; _⊔_) -open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder; SymmetricMonoidalMonotone) +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 @@ -38,7 +39,7 @@ private } where open SymmetricMonoidalPreorder A using (monoidalPreorder) - open Category (MonoidalPreorders c ℓ) using (id) + open Category (Monoidals c ℓ) using (id) compose : {c ℓ : Level} @@ -52,7 +53,7 @@ private where module G = SymmetricMonoidalMonotone G module F = SymmetricMonoidalMonotone F - open Category (MonoidalPreorders c ℓ) using (_∘_) + open Category (Monoidals c ℓ) using (_∘_) compose-resp-≃ : {c ℓ : Level} @@ -64,10 +65,10 @@ private → 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 Category (Monoidals _ _) open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM) --- The category of symmetric monoidal preorders +-- 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 ℓ 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/Preorders/Primitive.agda b/Category/Instance/Preorder/Primitive/Preorders.agda index 9c36d03..9832376 100644 --- a/Category/Instance/Preorders/Primitive.agda +++ b/Category/Instance/Preorder/Primitive/Preorders.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -module Category.Instance.Preorders.Primitive where +module Category.Instance.Preorder.Primitive.Preorders where open import Categories.Category using (Category) open import Categories.Category.Helper using (categoryHelper) 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/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/Lax.agda index ca03786..be4e835 100644 --- a/Functor/Free/Instance/MonoidalPreorder.agda +++ b/Functor/Free/Instance/MonoidalPreorder/Lax.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -module Functor.Free.Instance.MonoidalPreorder where +module Functor.Free.Instance.MonoidalPreorder.Lax where import Categories.Category.Monoidal.Utilities as ⊗-Util @@ -11,10 +11,11 @@ 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 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; MonoidalMonotone) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (MonoidalMonotone) open Lax using (MonoidalNaturalIsomorphism) @@ -61,7 +62,7 @@ module _ {o ℓ e : Level} where → 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 : {o ℓ e : Level} → Functor (Monoidals o ℓ e) (Monoidalsₚ o ℓ) Free = record { F₀ = monoidalPreorder ; F₁ = monoidalMonotone @@ -70,6 +71,6 @@ Free = record ; F-resp-≈ = pointwiseIsomorphism } where - open Category (MonoidalPreorders _ _) using (id) + 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/Lax.agda index 2fcecce..8bf567d 100644 --- a/Functor/Free/Instance/SymmetricMonoidalPreorder.agda +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda @@ -1,8 +1,8 @@ {-# OPTIONS --without-K --safe #-} -module Functor.Free.Instance.SymmetricMonoidalPreorder where +module Functor.Free.Instance.SymmetricMonoidalPreorder.Lax where -import Functor.Free.Instance.MonoidalPreorder as MP +import Functor.Free.Instance.MonoidalPreorder.Lax as MP open import Categories.Category using (Category) open import Category.Instance.SymMonCat using (SymMonCat) @@ -11,10 +11,11 @@ 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 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; SymmetricMonoidalMonotone) +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) 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 |