Differentiate lax and strong monoidal monotones

1 files changed, 0 insertions, 75 deletions

diff --git a/Functor/Free/Instance/MonoidalPreorder.agda b/Functor/Free/Instance/MonoidalPreorder.agda
deleted file mode 100644
index ca03786..0000000
--- a/Functor/Free/Instance/MonoidalPreorder.agda
+++ /dev/null
@@ -1,75 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Functor.Free.Instance.MonoidalPreorder where
-
-import Categories.Category.Monoidal.Utilities as ⊗-Util
-
-open import Categories.Category using (Category)
-open import Categories.Category.Instance.Monoidals using (Monoidals)
-open import Categories.Category.Monoidal using (MonoidalCategory)
-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 Data.Product using (_,_)
-open import Level using (Level)
-open import Preorder.Primitive.Monoidal using (MonoidalPreorder; MonoidalMonotone)
-
-open Lax using (MonoidalNaturalIsomorphism)
- 
--- The free monoidal preorder of a monoidal category
-
-import Functor.Free.Instance.Preorder as Preorder
-
-module _ {o ℓ e : Level} where
-
-  monoidalPreorder : MonoidalCategory o ℓ e → MonoidalPreorder o ℓ
-  monoidalPreorder C = record
-      { U = Preorder.Free.₀ U
-      ; monoidal = record
-          { unit = unit
-          ; tensor = Preorder.Free.₁ ⊗
-          ; unitaryˡ = Preorder.Free.F-resp-≈ unitorˡ-naturalIsomorphism
-          ; unitaryʳ = Preorder.Free.F-resp-≈ unitorʳ-naturalIsomorphism
-          ; associative = λ x y z → record
-              { from = associator.from {x} {y} {z}
-              ; to = associator.to {x} {y} {z}
-              }
-          }
-      }
-    where
-      open MonoidalCategory C
-      open ⊗-Util monoidal
-
-  module _ {A B : MonoidalCategory o ℓ e} where
-
-    monoidalMonotone : MonoidalFunctor A B → MonoidalMonotone (monoidalPreorder A) (monoidalPreorder B)
-    monoidalMonotone F = record
-        { F = Preorder.Free.₁ F.F
-        ; ε = F.ε
-        ; ⊗-homo = λ p₁ p₂ → F.⊗-homo.η (p₁ , p₂)
-        }
-      where
-        module F = MonoidalFunctor F
-
-    open MonoidalNaturalIsomorphism using (U)
-
-    pointwiseIsomorphism
-        : {F G : MonoidalFunctor A B}
-        → MonoidalNaturalIsomorphism F G
-        → 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 = record
-    { F₀ = monoidalPreorder
-    ; F₁ = monoidalMonotone
-    ; identity = λ {A} → ≃.refl {A = monoidalPreorder A} {x = id}
-    ; homomorphism = λ {f = f} {h} → ≃.refl {x = monoidalMonotone (∘-Monoidal h f)}
-    ; F-resp-≈ = pointwiseIsomorphism
-    }
-  where
-    open Category (MonoidalPreorders _ _) using (id)
-
-module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})