Differentiate lax and strong monoidal monotones

3 files changed, 100 insertions, 52 deletions

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