From b2c2426959715260f57153b91ce11d12c7fdb298 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 7 Jan 2026 10:52:51 -0600 Subject: Add strong variants of cats to preorders functors --- Functor/Free/Instance/MonoidalPreorder/Strong.agda | 77 ++++++++++++++++++++++ .../Instance/SymmetricMonoidalPreorder/Lax.agda | 4 +- .../Instance/SymmetricMonoidalPreorder/Strong.agda | 68 +++++++++++++++++++ 3 files changed, 147 insertions(+), 2 deletions(-) create mode 100644 Functor/Free/Instance/MonoidalPreorder/Strong.agda create mode 100644 Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda (limited to 'Functor/Free') diff --git a/Functor/Free/Instance/MonoidalPreorder/Strong.agda b/Functor/Free/Instance/MonoidalPreorder/Strong.agda new file mode 100644 index 0000000..612e91c --- /dev/null +++ b/Functor/Free/Instance/MonoidalPreorder/Strong.agda @@ -0,0 +1,77 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Free.Instance.MonoidalPreorder.Strong where + +import Categories.Category.Monoidal.Utilities as ⊗-Util +import Functor.Free.Instance.Preorder as Preorder + +open import Categories.Category using (Category) +open import Categories.Category.Instance.Monoidals using (StrongMonoidals) +open import Categories.Category.Monoidal using (MonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.Functor.Monoidal using (StrongMonoidalFunctor) +open import Categories.Functor.Monoidal.Properties using (∘-StrongMonoidal) +open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using (module Strong) +open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (_≃_; module ≃) renaming (Monoidals to Monoidalsₚ) +open import Data.Product using (_,_) +open import Level using (Level) +open import Preorder.Primitive using (module Isomorphism) +open import Preorder.Primitive.MonotoneMap using (MonotoneMap) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder) +open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (MonoidalMonotone) + +open Strong using (MonoidalNaturalIsomorphism) +  +-- The free monoidal preorder of a monoidal category + +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 : StrongMonoidalFunctor A B → MonoidalMonotone (monoidalPreorder A) (monoidalPreorder B) + monoidalMonotone F = record + { F = Preorder.Free.₁ F.F + ; ε = record { F.ε } + ; ⊗-homo = λ p₁ p₂ → Preorder.Free.F-resp-≈ F.⊗-homo (p₁ , p₂) + } + where + module F = StrongMonoidalFunctor F + + open MonoidalNaturalIsomorphism using (U) + + pointwiseIsomorphism + : {F G : StrongMonoidalFunctor A B} + → MonoidalNaturalIsomorphism F G + → monoidalMonotone F ≃ monoidalMonotone G + pointwiseIsomorphism F≃G = Preorder.Free.F-resp-≈ (U F≃G) + +Free : {o ℓ e : Level} → Functor (StrongMonoidals 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 (∘-StrongMonoidal 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/SymmetricMonoidalPreorder/Lax.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda index 8bf567d..ebb3dc0 100644 --- a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda @@ -5,7 +5,7 @@ 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 Category.Instance.SymMonCat using (module Lax) 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₁) @@ -54,7 +54,7 @@ module _ {o ℓ e : Level} where → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋ -Free : {o ℓ e : Level} → Functor (SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) +Free : {o ℓ e : Level} → Functor (Lax.SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) Free = record { F₀ = symmetricMonoidalPreorder ; F₁ = symmetricMonoidalMonotone diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda new file mode 100644 index 0000000..f759f17 --- /dev/null +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda @@ -0,0 +1,68 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Free.Instance.SymmetricMonoidalPreorder.Strong where + +import Functor.Free.Instance.MonoidalPreorder.Strong as MP + +open import Categories.Category using (Category) +open import Category.Instance.SymMonCat using (module Strong) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.Functor.Monoidal.Symmetric using () renaming (module Strong to Strong₁) +open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-StrongSymmetricMonoidal) +open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Strong to Strong₂) +open import Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Strong 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.Strong using (SymmetricMonoidalMonotone) + +open Strong₁ using (SymmetricMonoidalFunctor) +open Strong₂ 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 (Strong.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 (∘-StrongSymmetricMonoidal h f)} + ; F-resp-≈ = pointwiseIsomorphism + } + where + open Category (SymMonPre _ _) using (id) + +module Free {o ℓ e} = Functor (Free {o} {ℓ} {e}) -- cgit v1.2.3