diff options
| -rw-r--r-- | Category/Instance/SymMonCat.agda | 174 | ||||
| -rw-r--r-- | Functor/Free/Instance/MonoidalPreorder/Strong.agda | 77 | ||||
| -rw-r--r-- | Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda | 4 | ||||
| -rw-r--r-- | Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda | 68 |
4 files changed, 265 insertions, 58 deletions
diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda index 814abeb..6693639 100644 --- a/Category/Instance/SymMonCat.agda +++ b/Category/Instance/SymMonCat.agda @@ -16,59 +16,121 @@ open import Relation.Binary.Core using (Rel) open import Categories.Category using (Category; _[_,_]; _[_∘_]) open import Categories.Category.Helper using (categoryHelper) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) -open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) - -open SMF.Lax using (SymmetricMonoidalFunctor) -open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) - -assoc - : {A B C D : SymmetricMonoidalCategory o ℓ e} - {F : SymmetricMonoidalFunctor A B} - {G : SymmetricMonoidalFunctor B C} - {H : SymmetricMonoidalFunctor C D} - → SymmetricMonoidalNaturalIsomorphism - (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F) - (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F)) -assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H} - -identityˡ - : {A B : SymmetricMonoidalCategory o ℓ e} - {F : SymmetricMonoidalFunctor A B} - → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F -identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} - -identityʳ - : {A B : SymmetricMonoidalCategory o ℓ e} - {F : SymmetricMonoidalFunctor A B} - → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F -identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} - -Compose - : {A B C : SymmetricMonoidalCategory o ℓ e} - → SymmetricMonoidalFunctor B C - → SymmetricMonoidalFunctor A B - → SymmetricMonoidalFunctor A C -Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G - -∘-resp-≈ - : {A B C : SymmetricMonoidalCategory o ℓ e} - {f h : SymmetricMonoidalFunctor B C} - {g i : SymmetricMonoidalFunctor A B} - → SymmetricMonoidalNaturalIsomorphism f h - → SymmetricMonoidalNaturalIsomorphism g i - → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i) -∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′ - -SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) -SymMonCat = categoryHelper record - { Obj = SymmetricMonoidalCategory o ℓ e - ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e} - ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} } - ; id = λ { {X} → idF-SymmetricMonoidal X } - ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G } - ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} } - ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} } - ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} } - ; equiv = isEquivalence - ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i } - } +open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; idF-StrongSymmetricMonoidal; ∘-SymmetricMonoidal; ∘-StrongSymmetricMonoidal) + + +-- Category of symmetric monoidal categories and lax symmetric monoidal functors + +module Lax where + + open SMF.Lax using (SymmetricMonoidalFunctor) + open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + + assoc + : {A B C D : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + {G : SymmetricMonoidalFunctor B C} + {H : SymmetricMonoidalFunctor C D} + → SymmetricMonoidalNaturalIsomorphism + (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F) + (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F)) + assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H} + + identityˡ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F + identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + + identityʳ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F + identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + + Compose + : {A B C : SymmetricMonoidalCategory o ℓ e} + → SymmetricMonoidalFunctor B C + → SymmetricMonoidalFunctor A B + → SymmetricMonoidalFunctor A C + Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G + + ∘-resp-≈ + : {A B C : SymmetricMonoidalCategory o ℓ e} + {f h : SymmetricMonoidalFunctor B C} + {g i : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism f h + → SymmetricMonoidalNaturalIsomorphism g i + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i) + ∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′ + + SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) + SymMonCat = categoryHelper record + { Obj = SymmetricMonoidalCategory o ℓ e + ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e} + ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} } + ; id = λ { {X} → idF-SymmetricMonoidal X } + ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G } + ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} } + ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} } + ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} } + ; equiv = isEquivalence + ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i } + } + +module Strong where + + open SMF.Strong using (SymmetricMonoidalFunctor) + open SMNI.Strong using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + + assoc + : {A B C D : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + {G : SymmetricMonoidalFunctor B C} + {H : SymmetricMonoidalFunctor C D} + → SymmetricMonoidalNaturalIsomorphism + (∘-StrongSymmetricMonoidal (∘-StrongSymmetricMonoidal H G) F) + (∘-StrongSymmetricMonoidal H (∘-StrongSymmetricMonoidal G F)) + assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Strong.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H} + + identityˡ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal (idF-StrongSymmetricMonoidal B) F) F + identityˡ {A} {B} {F} = SMNI.Strong.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + + identityʳ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal F (idF-StrongSymmetricMonoidal A)) F + identityʳ {A} {B} {F} = SMNI.Strong.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + + Compose + : {A B C : SymmetricMonoidalCategory o ℓ e} + → SymmetricMonoidalFunctor B C + → SymmetricMonoidalFunctor A B + → SymmetricMonoidalFunctor A C + Compose {A} {B} {C} F G = ∘-StrongSymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G + + ∘-resp-≈ + : {A B C : SymmetricMonoidalCategory o ℓ e} + {f h : SymmetricMonoidalFunctor B C} + {g i : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism f h + → SymmetricMonoidalNaturalIsomorphism g i + → SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal f g) (∘-StrongSymmetricMonoidal h i) + ∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Strong._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′ + + SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) + SymMonCat = categoryHelper record + { Obj = SymmetricMonoidalCategory o ℓ e + ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e} + ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} } + ; id = λ { {X} → idF-StrongSymmetricMonoidal X } + ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G } + ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} } + ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} } + ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} } + ; equiv = isEquivalence + ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i } + } 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}) |