Differentiate lax and strong monoidal monotones

4 files changed, 13 insertions, 11 deletions

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)