Differentiate lax and strong monoidal monotones

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