Differentiate lax and strong monoidal monotones

1 files changed, 16 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