From 8ec259bb32b4339b27560f5ea13afa81b9b8febc Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 7 Jan 2026 10:12:13 -0600 Subject: Differentiate lax and strong monoidal monotones --- Functor/Free/Instance/InducedSetoid.agda | 2 +- Functor/Free/Instance/MonoidalPreorder.agda | 75 --------------------- Functor/Free/Instance/MonoidalPreorder/Lax.agda | 76 ++++++++++++++++++++++ Functor/Free/Instance/Preorder.agda | 2 +- .../Free/Instance/SymmetricMonoidalPreorder.agda | 67 ------------------- .../Instance/SymmetricMonoidalPreorder/Lax.agda | 68 +++++++++++++++++++ 6 files changed, 146 insertions(+), 144 deletions(-) delete mode 100644 Functor/Free/Instance/MonoidalPreorder.agda create mode 100644 Functor/Free/Instance/MonoidalPreorder/Lax.agda delete mode 100644 Functor/Free/Instance/SymmetricMonoidalPreorder.agda create mode 100644 Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda (limited to 'Functor/Free') 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.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}) diff --git a/Functor/Free/Instance/MonoidalPreorder/Lax.agda b/Functor/Free/Instance/MonoidalPreorder/Lax.agda new file mode 100644 index 0000000..be4e835 --- /dev/null +++ b/Functor/Free/Instance/MonoidalPreorder/Lax.agda @@ -0,0 +1,76 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Free.Instance.MonoidalPreorder.Lax 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.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) +open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (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) (Monoidalsₚ 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 (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.agda deleted file mode 100644 index 2fcecce..0000000 --- a/Functor/Free/Instance/SymmetricMonoidalPreorder.agda +++ /dev/null @@ -1,67 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Functor.Free.Instance.SymmetricMonoidalPreorder where - -import Functor.Free.Instance.MonoidalPreorder as MP - -open import Categories.Category using (Category) -open import Category.Instance.SymMonCat using (SymMonCat) -open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) -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 Data.Product using (_,_) -open import Level using (Level) -open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder; SymmetricMonoidalMonotone) - -open Lax₁ using (SymmetricMonoidalFunctor) -open Lax₂ using (SymmetricMonoidalNaturalIsomorphism) -  --- The free symmetric monoidal preorder of a symmetric monoidal category - -module _ {o ℓ e : Level} where - - symmetricMonoidalPreorder : SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalPreorder o ℓ - symmetricMonoidalPreorder C = record - { M - ; symmetric = record - { symmetric = λ x y → braiding.⇒.η (x , y) - } - } - where - open SymmetricMonoidalCategory C - module M = MonoidalPreorder (MP.Free.₀ monoidalCategory) - - module _ {A B : SymmetricMonoidalCategory o ℓ e} where - - symmetricMonoidalMonotone - : SymmetricMonoidalFunctor A B - → SymmetricMonoidalMonotone (symmetricMonoidalPreorder A) (symmetricMonoidalPreorder B) - symmetricMonoidalMonotone F = record - { monoidalMonotone = MP.Free.₁ F.monoidalFunctor - } - where - module F = SymmetricMonoidalFunctor F - - open SymmetricMonoidalNaturalIsomorphism using (⌊_⌋) - - pointwiseIsomorphism - : {F G : SymmetricMonoidalFunctor A B} - → SymmetricMonoidalNaturalIsomorphism F G - → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G - pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋ - -Free : {o ℓ e : Level} → Functor (SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) -Free = record - { F₀ = symmetricMonoidalPreorder - ; F₁ = symmetricMonoidalMonotone - ; identity = λ {A} → ≃.refl {A = symmetricMonoidalPreorder A} {x = id} - ; homomorphism = λ {f = f} {h} → ≃.refl {x = symmetricMonoidalMonotone (∘-SymmetricMonoidal h f)} - ; F-resp-≈ = pointwiseIsomorphism - } - where - open Category (SymMonPre _ _) using (id) - -module Free {o ℓ e} = Functor (Free {o} {ℓ} {e}) diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda new file mode 100644 index 0000000..8bf567d --- /dev/null +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda @@ -0,0 +1,68 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Free.Instance.SymmetricMonoidalPreorder.Lax where + +import Functor.Free.Instance.MonoidalPreorder.Lax as MP + +open import Categories.Category using (Category) +open import Category.Instance.SymMonCat using (SymMonCat) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +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.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) +open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (SymmetricMonoidalMonotone) + +open Lax₁ using (SymmetricMonoidalFunctor) +open Lax₂ using (SymmetricMonoidalNaturalIsomorphism) +  +-- The free symmetric monoidal preorder of a symmetric monoidal category + +module _ {o ℓ e : Level} where + + symmetricMonoidalPreorder : SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalPreorder o ℓ + symmetricMonoidalPreorder C = record + { M + ; symmetric = record + { symmetric = λ x y → braiding.⇒.η (x , y) + } + } + where + open SymmetricMonoidalCategory C + module M = MonoidalPreorder (MP.Free.₀ monoidalCategory) + + module _ {A B : SymmetricMonoidalCategory o ℓ e} where + + symmetricMonoidalMonotone + : SymmetricMonoidalFunctor A B + → SymmetricMonoidalMonotone (symmetricMonoidalPreorder A) (symmetricMonoidalPreorder B) + symmetricMonoidalMonotone F = record + { monoidalMonotone = MP.Free.₁ F.monoidalFunctor + } + where + module F = SymmetricMonoidalFunctor F + + open SymmetricMonoidalNaturalIsomorphism using (⌊_⌋) + + pointwiseIsomorphism + : {F G : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism F G + → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G + pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋ + +Free : {o ℓ e : Level} → Functor (SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) +Free = record + { F₀ = symmetricMonoidalPreorder + ; F₁ = symmetricMonoidalMonotone + ; identity = λ {A} → ≃.refl {A = symmetricMonoidalPreorder A} {x = id} + ; homomorphism = λ {f = f} {h} → ≃.refl {x = symmetricMonoidalMonotone (∘-SymmetricMonoidal h f)} + ; F-resp-≈ = pointwiseIsomorphism + } + where + open Category (SymMonPre _ _) using (id) + +module Free {o ℓ e} = Functor (Free {o} {ℓ} {e}) -- cgit v1.2.3