diff options
Diffstat (limited to 'Functor')
| -rw-r--r-- | Functor/Instance/CMonoidalize.agda | 42 | ||||
| -rw-r--r-- | Functor/Monoidal/Construction/CMonoidValued.agda | 100 |
2 files changed, 142 insertions, 0 deletions
diff --git a/Functor/Instance/CMonoidalize.agda b/Functor/Instance/CMonoidalize.agda new file mode 100644 index 0000000..41eb4e4 --- /dev/null +++ b/Functor/Instance/CMonoidalize.agda @@ -0,0 +1,42 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +open import Categories.Category using (Category) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Category.Cocartesian using (Cocartesian) + +module Functor.Instance.CMonoidalize + {o o′ ℓ ℓ′ e e ′ : Level} + {C : Category o ℓ e} + (cocartesian : Cocartesian C) + (D : SymmetricMonoidalCategory o ℓ e) + where + +open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal) +open import Categories.Functor using (Functor) +open import Category.Construction.CMonoids using (CMonoids) +open import Categories.Category.Construction.Functors using (Functors) +open import Category.Construction.SymmetricMonoidalFunctors using (module Lax) +open import Functor.Monoidal.Construction.CMonoidValued cocartesian {D} using () renaming (F,⊗,ε,σ to SMFOf) +open import NaturalTransformation.Monoidal.Construction.CMonoidValued cocartesian {D} using () renaming (β,⊗,ε,σ to SMNTOf) + +private + + open CocartesianSymmetricMonoidal C cocartesian + + C-SMC : SymmetricMonoidalCategory o ℓ e + C-SMC = record { symmetric = +-symmetric } + + module C = SymmetricMonoidalCategory C-SMC + module D = SymmetricMonoidalCategory D + +open Functor + +CMonoidalize : Functor (Functors C.U (CMonoids D.symmetric)) (Lax.SymmetricMonoidalFunctors C-SMC D) +CMonoidalize .F₀ = SMFOf +CMonoidalize .F₁ α = SMNTOf α +CMonoidalize .identity = D.Equiv.refl +CMonoidalize .homomorphism = D.Equiv.refl +CMonoidalize .F-resp-≈ x = x + +module CMonoidalize = Functor CMonoidalize diff --git a/Functor/Monoidal/Construction/CMonoidValued.agda b/Functor/Monoidal/Construction/CMonoidValued.agda new file mode 100644 index 0000000..2ac8be2 --- /dev/null +++ b/Functor/Monoidal/Construction/CMonoidValued.agda @@ -0,0 +1,100 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Category.Construction.CMonoids using (CMonoids) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_) +open import Level using (Level; _⊔_) + +-- A functor from a cocartesian category 𝒞 to CMonoids[S] +-- can be turned into a symmetric monoidal functor from 𝒞 to S + +module Functor.Monoidal.Construction.CMonoidValued + {o o′ ℓ ℓ′ e e′ : Level} + {𝒞 : Category o ℓ e} + (𝒞-+ : Cocartesian 𝒞) + {S : SymmetricMonoidalCategory o′ ℓ′ e′} + (let module S = SymmetricMonoidalCategory S) + (M : Functor 𝒞 (CMonoids S.symmetric)) + where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Object.Monoid.Commutative as CommutativeMonoidObject +import Functor.Monoidal.Construction.MonoidValued as MonoidValued + +open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.Functor.Properties using ([_]-resp-∘) +open import Data.Product using (_,_) +open import Functor.Forgetful.Instance.CMonoid S.symmetric using (Forget) +open import Functor.Forgetful.Instance.Monoid S.monoidal using () renaming (Forget to Forgetₘ) + +private + + G : Functor 𝒞 (Monoids S.monoidal) + G = Forget ∙ M + + H : Functor 𝒞 S.U + H = Forgetₘ ∙ G + + module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ }) + module 𝒞-SM = CocartesianSymmetricMonoidal 𝒞 𝒞-+ + + 𝒞-SMC : SymmetricMonoidalCategory o ℓ e + 𝒞-SMC = record { symmetric = 𝒞-SM.+-symmetric } + + module H = Functor H + module M = Functor M + + open CommutativeMonoidObject S.symmetric using (CommutativeMonoid; CommutativeMonoid⇒) + open CommutativeMonoid using (μ; Carrier) renaming (commutative to μ-commutative) + open CommutativeMonoid⇒ + open 𝒞 using (_+_; i₁; i₂; inject₁; inject₂; +-swap) + open S + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open Shorthands symmetric + + ⊲ : {A : 𝒞.Obj} → H.₀ A ⊗₀ H.₀ A ⇒ H.₀ A + ⊲ {A} = μ (M.₀ A) + + ⇒⊲ : {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) → H.₁ f ∘ ⊲ ≈ ⊲ ∘ H.₁ f ⊗₁ H.₁ f + ⇒⊲ f = preserves-μ (M.₁ f) + + ⊲-⊗ : {n m : 𝒞.Obj} → H.₀ n ⊗₀ H.₀ m ⇒ H.₀ (n + m) + ⊲-⊗ = ⊲ ∘ H.₁ i₁ ⊗₁ H.₁ i₂ + + ⊲-σ : {n : 𝒞.Obj} → ⊲ {n} ≈ ⊲ ∘ σ⇒ + ⊲-σ {A} = μ-commutative (M.₀ A) + + braiding-compat + : {n m : 𝒞.Obj} + → H.₁ +-swap ∘ ⊲-⊗ {n} {m} + ≈ ⊲-⊗ ∘ σ⇒ {H.₀ n} {H.₀ m} + braiding-compat {n} {m} = begin + H.₁ +-swap ∘ ⊲-⊗ {n} {m} ≡⟨⟩ + H.₁ +-swap ∘ ⊲ {n + m} ∘ H.₁ i₁ ⊗₁ H.₁ i₂ ≈⟨ extendʳ (⇒⊲ +-swap) ⟩ + ⊲ {m + n} ∘ H.₁ +-swap ⊗₁ H.₁ +-swap ∘ H.₁ i₁ ⊗₁ H.₁ i₂ ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + ⊲ {m + n} ∘ (H.₁ +-swap ∘ H.₁ i₁) ⊗₁ (H.₁ +-swap ∘ H.₁ i₂) ≈⟨ refl⟩∘⟨ [ H ]-resp-∘ inject₁ ⟩⊗⟨ [ H ]-resp-∘ inject₂ ⟩ + ⊲ {m + n} ∘ H.₁ i₂ ⊗₁ H.₁ i₁ ≈⟨ ⊲-σ ⟩∘⟨refl ⟩ + (⊲ {m + n} ∘ σ⇒) ∘ H.₁ i₂ ⊗₁ H.₁ i₁ ≈⟨ extendˡ (braiding.⇒.commute (H.₁ i₂ , H.₁ i₁)) ⟩ + (⊲ {m + n} ∘ H.₁ i₁ ⊗₁ H.₁ i₂) ∘ σ⇒ ≡⟨⟩ + ⊲-⊗ {m} {n} ∘ σ⇒ {H.₀ n} {H.₀ m} ∎ + +open MonoidValued 𝒞-+ G using (F,⊗,ε) + +F,⊗,ε,σ : Lax.SymmetricMonoidalFunctor 𝒞-SMC S +F,⊗,ε,σ = record + { F,⊗,ε + ; isBraidedMonoidal = record + { F,⊗,ε + ; braiding-compat = braiding-compat + } + } + +module F,⊗,ε,σ = Lax.SymmetricMonoidalFunctor F,⊗,ε,σ |