From 9fe4aadad5a046aaf44a789bfddefc10a0afaeef Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 14 Nov 2025 12:53:49 -0600 Subject: Generalize ListOf construction to arbitrary monoid --- Functor/Monoidal/Construction/FamilyOfMonoids.agda | 214 +++++++++++++++++++++ Functor/Monoidal/Construction/ListOf.agda | 213 -------------------- 2 files changed, 214 insertions(+), 213 deletions(-) create mode 100644 Functor/Monoidal/Construction/FamilyOfMonoids.agda delete mode 100644 Functor/Monoidal/Construction/ListOf.agda (limited to 'Functor') diff --git a/Functor/Monoidal/Construction/FamilyOfMonoids.agda b/Functor/Monoidal/Construction/FamilyOfMonoids.agda new file mode 100644 index 0000000..377342a --- /dev/null +++ b/Functor/Monoidal/Construction/FamilyOfMonoids.agda @@ -0,0 +1,214 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory) +open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_) +open import Level using (Level; _⊔_) + +-- A functor from a cocartesian category 𝒞 to Monoids[S] +-- can be turned into a monoidal functor from 𝒞 to S + +module Functor.Monoidal.Construction.FamilyOfMonoids + {o o′ ℓ ℓ′ e e′ : Level} + {𝒞 : Category o ℓ e} + (𝒞-+ : Cocartesian 𝒞) + {S : MonoidalCategory o′ ℓ′ e′} + (let module S = MonoidalCategory S) + (M : Functor 𝒞 (Monoids S.monoidal)) + where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Category.Monoidal.Utilities as ⊗-Util +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Object.Monoid as MonoidObject + +open import Categories.Category using (module Definitions) +open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor.Monoidal using (MonoidalFunctor; IsMonoidalFunctor) +open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) +open import Categories.Morphism using (_≅_) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Data.Product using (_,_) +open import Functor.Forgetful.Instance.Monoid S using (Forget) + +private + + G : Functor 𝒞 S.U + G = Forget ∙ M + + module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ }) + module 𝒞-M = CocartesianMonoidal 𝒞 𝒞-+ + + 𝒞-MC : MonoidalCategory o ℓ e + 𝒞-MC = record { monoidal = 𝒞-M.+-monoidal } + + module +-assoc {n} {m} {o} = _≅_ (𝒞.+-assoc {n} {m} {o}) + module +-λ {n} = _≅_ (𝒞-M.⊥+A≅A {n}) + module +-ρ {n} = _≅_ (𝒞-M.A+⊥≅A {n}) + + module G = Functor G + module M = Functor M + + open MonoidObject S.monoidal using (Monoid; Monoid⇒) + open Monoid renaming (assoc to μ-assoc; identityˡ to μ-identityˡ; identityʳ to μ-identityʳ) + open Monoid⇒ + + open 𝒞 using (-+-; _+_; _+₁_; i₁; i₂; inject₁; inject₂) + + module _ where + + open Category 𝒞 + open ⇒-Reasoning 𝒞 + open ⊗-Reasoning 𝒞-M.+-monoidal + + module _ {n m o : Obj} where + + private + + +-α : (n + m) + o 𝒞.⇒ n + (m + o) + +-α = +-assoc.to {n} {m} {o} + + +-α∘i₂ : +-α ∘ i₂ ≈ i₂ ∘ i₂ + +-α∘i₂ = inject₂ + + +-α∘i₁∘i₁ : (+-α ∘ i₁) ∘ i₁ ≈ i₁ + +-α∘i₁∘i₁ = inject₁ ⟩∘⟨refl ○ inject₁ + + +-α∘i₁∘i₂ : (+-α ∘ i₁) ∘ i₂ ≈ i₂ ∘ i₁ + +-α∘i₁∘i₂ = inject₁ ⟩∘⟨refl ○ inject₂ + + module _ {n : Obj} where + + +-ρ∘i₁ : +-ρ.from {n} ∘ i₁ ≈ id + +-ρ∘i₁ = inject₁ + + +-λ∘i₂ : +-λ.from {n} ∘ i₂ ≈ id + +-λ∘i₂ = inject₂ + + open S + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open ⊗-Util.Shorthands monoidal + + ⊲ : {A : 𝒞.Obj} → G.₀ A ⊗₀ G.₀ A ⇒ G.₀ A + ⊲ {A} = μ (M.₀ A) + + ⇒⊲ : {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) → G.₁ f ∘ ⊲ ≈ ⊲ ∘ G.₁ f ⊗₁ G.₁ f + ⇒⊲ f = preserves-μ (M.₁ f) + + ε : {A : 𝒞.Obj} → unit ⇒ G.₀ A + ε {A} = η (M.₀ A) + + ⇒ε : {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) → G.₁ f ∘ ε ≈ ε + ⇒ε f = preserves-η (M.₁ f) + + ⊲-⊗ : {n m : 𝒞.Obj} → G.₀ n ⊗₀ G.₀ m ⇒ G.₀ (n + m) + ⊲-⊗ = ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂ + + module _ {n n′ m m′ : 𝒞.Obj} (f : n 𝒞.⇒ n′) (g : m 𝒞.⇒ m′) where + + open Definitions S.U using (CommutativeSquare) + + left₁ : CommutativeSquare (G.₁ i₁) (G.₁ f) (G.₁ (f +₁ g)) (G.₁ i₁) + left₁ = [ G ]-resp-square inject₁ + + left₂ : CommutativeSquare (G.₁ i₂) (G.₁ g) (G.₁ (f +₁ g)) (G.₁ i₂) + left₂ = [ G ]-resp-square inject₂ + + right : CommutativeSquare ⊲ (G.₁ (f +₁ g) ⊗₁ G.₁ (f +₁ g)) (G.₁ (f +₁ g)) ⊲ + right = ⇒⊲ (f +₁ g) + + ⊲-⊗-commute : + CommutativeSquare + (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + (G.₁ f ⊗₁ G.₁ g) + (G.₁ (f +₁ g)) + (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ⊲-⊗-commute = glue′ right (parallel left₁ left₂) + + ⊲-⊗-homo : NaturalTransformation (⊗ ∙ (G ⁂ G)) (G ∙ -+-) + ⊲-⊗-homo = ntHelper record + { η = λ (n , m) → ⊲-⊗ {n} {m} + ; commute = λ (f , g) → Equiv.sym (⊲-⊗-commute f g) + } + + ⊲-⊗-α + : {n m o : 𝒞.Obj} + → G.₁ (+-assoc.to {n} {m} {o}) + ∘ (μ (M.₀ ((n + m) + o)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ∘ (μ (M.₀ (n + m)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ id + ≈ (μ (M.₀ (n + m + o)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ∘ id ⊗₁ (μ (M.₀ (m + o)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ∘ α⇒ + ⊲-⊗-α {n} {m} {o} = begin + G.₁ +-α ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ id ≈⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ + G.₁ +-α ∘ ⊲ ∘ (G.₁ i₁ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ G.₁ i₂ ≈⟨ extendʳ (⇒⊲ +-α) ⟩ + ⊲ ∘ G.₁ +-α ⊗₁ G.₁ +-α ∘ (G.₁ i₁ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ G.₁ i₂ ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + ⊲ ∘ (G.₁ +-α ∘ G.₁ i₁ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ (G.₁ +-α ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ pullˡ (Equiv.sym G.homomorphism) ⟩⊗⟨ [ G ]-resp-square +-α∘i₂ ⟩ + ⊲ ∘ (G.₁ (+-α 𝒞.∘ i₁) ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ extendʳ (⇒⊲ (+-α 𝒞.∘ i₁)) ⟩⊗⟨refl ⟩ + ⊲ ∘ (⊲ ∘ G.₁ (+-α 𝒞.∘ i₁) ⊗₁ G.₁ (+-α 𝒞.∘ i₁) ∘ _) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩⊗⟨refl ⟨ + ⊲ ∘ (⊲ ∘ _ ⊗₁ (G.₁ (+-α 𝒞.∘ i₁) ∘ G.₁ i₂)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ [ G ]-resp-∘ +-α∘i₁∘i₁ ⟩⊗⟨ [ G ]-resp-square +-α∘i₁∘i₂) ⟩⊗⟨refl ⟩ + ⊲ ∘ (⊲ ∘ G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ split₁ˡ ⟩ + ⊲ ∘ ⊲ ⊗₁ id ∘ (G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ extendʳ (μ-assoc (M.₀ (n + (m + o)))) ⟩ + ⊲ ∘ (id ⊗₁ ⊲ ∘ α⇒) ∘ (G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ assoc ⟩ + ⊲ ∘ id ⊗₁ ⊲ ∘ α⇒ ∘ (G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟩ + ⊲ ∘ id ⊗₁ ⊲ ∘ G.₁ i₁ ⊗₁ ((G.₁ i₂ ∘ G.₁ i₁) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂)) ∘ α⇒ ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ + ⊲ ∘ G.₁ i₁ ⊗₁ (⊲ ∘ (G.₁ i₂ ∘ G.₁ i₁) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩∘⟨refl ⟩ + ⊲ ∘ G.₁ i₁ ⊗₁ (⊲ ∘ G.₁ i₂ ⊗₁ G.₁ i₂ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (extendʳ (⇒⊲ i₂)) ⟩∘⟨refl ⟨ + ⊲ ∘ G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ α⇒ ≈⟨ pushʳ (pushˡ split₂ʳ) ⟩ + (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ id ⊗₁ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ α⇒ ∎ + where + +-α : (n + m) + o 𝒞.⇒ n + (m + o) + +-α = +-assoc.to {n} {m} {o} + + module _ {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) where + + ⊲-εʳ : ⊲ ∘ G.₁ f ⊗₁ ε ≈ G.₁ f ∘ ρ⇒ + ⊲-εʳ = begin + ⊲ ∘ G.₁ f ⊗₁ ε ≈⟨ refl⟩∘⟨ serialize₂₁ ⟩ + ⊲ ∘ id ⊗₁ ε ∘ G.₁ f ⊗₁ id ≈⟨ pullˡ (Equiv.sym (μ-identityʳ (M.₀ B))) ⟩ + ρ⇒ ∘ G.₁ f ⊗₁ id ≈⟨ unitorʳ-commute-from ⟩ + G.₁ f ∘ ρ⇒ ∎ + + ⊲-εˡ : ⊲ ∘ ε ⊗₁ G.₁ f ≈ G.₁ f ∘ λ⇒ + ⊲-εˡ = begin + ⊲ ∘ ε ⊗₁ G.₁ f ≈⟨ refl⟩∘⟨ serialize₁₂ ⟩ + ⊲ ∘ ε ⊗₁ id ∘ id ⊗₁ G.₁ f ≈⟨ pullˡ (Equiv.sym (μ-identityˡ (M.₀ B))) ⟩ + λ⇒ ∘ id ⊗₁ G.₁ f ≈⟨ unitorˡ-commute-from ⟩ + G.₁ f ∘ λ⇒ ∎ + + module _ {n : 𝒞.Obj} where + + ⊲-⊗-λ : G.₁ (+-λ.from {n}) ∘ ⊲-⊗ ∘ ε ⊗₁ id ≈ λ⇒ + ⊲-⊗-λ = begin + G.₁ +-λ.from ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ + G.₁ +-λ.from ∘ ⊲ ∘ (G.₁ i₁ ∘ ε) ⊗₁ G.₁ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⇒ε i₁ ⟩⊗⟨refl ⟩ + G.₁ +-λ.from ∘ ⊲ ∘ ε ⊗₁ G.₁ i₂ ≈⟨ refl⟩∘⟨ ⊲-εˡ i₂ ⟩ + G.₁ +-λ.from ∘ G.₁ i₂ ∘ λ⇒ ≈⟨ cancelˡ ([ G ]-resp-∘ +-λ∘i₂ ○ G.identity) ⟩ + λ⇒ ∎ + + ⊲-⊗-ρ : G.₁ (+-ρ.from {n}) ∘ ⊲-⊗ ∘ id ⊗₁ ε ≈ ρ⇒ + ⊲-⊗-ρ = begin + G.₁ +-ρ.from ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ pullʳ merge₂ʳ ⟩ + G.₁ +-ρ.from ∘ ⊲ ∘ G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⇒ε i₂ ⟩ + G.₁ +-ρ.from ∘ ⊲ ∘ G.₁ i₁ ⊗₁ ε ≈⟨ refl⟩∘⟨ ⊲-εʳ i₁ ⟩ + G.₁ +-ρ.from ∘ G.₁ i₁ ∘ ρ⇒ ≈⟨ cancelˡ ([ G ]-resp-∘ +-ρ∘i₁ ○ G.identity) ⟩ + ρ⇒   ∎ + +F,⊗,ε : MonoidalFunctor 𝒞-MC S +F,⊗,ε = record + { F = G + ; isMonoidal = record + { ε = ε + ; ⊗-homo = ⊲-⊗-homo + ; associativity = ⊲-⊗-α + ; unitaryˡ = ⊲-⊗-λ + ; unitaryʳ = ⊲-⊗-ρ  + } + } + +module F,⊗,ε = MonoidalFunctor F,⊗,ε diff --git a/Functor/Monoidal/Construction/ListOf.agda b/Functor/Monoidal/Construction/ListOf.agda deleted file mode 100644 index 23c6ba8..0000000 --- a/Functor/Monoidal/Construction/ListOf.agda +++ /dev/null @@ -1,213 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Categories.Category using (Category) -open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) -open import Categories.Category.Construction.Monoids using (Monoids) -open import Categories.Category.Monoidal.Bundle using (MonoidalCategory) -open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_) -open import Level using (Level) - -module Functor.Monoidal.Construction.ListOf - {o o′ ℓ ℓ′ e e′ : Level} - {𝒞 : CocartesianCategory o ℓ e} - {S : MonoidalCategory o′ ℓ′ e′} - (let module 𝒞 = CocartesianCategory 𝒞) - (let module S = MonoidalCategory S) - (G : Functor 𝒞.U S.U) - (M : Functor S.U (Monoids S.monoidal)) - where - -import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning -import Categories.Category.Monoidal.Utilities as ⊗-Util -import Categories.Morphism.Reasoning as ⇒-Reasoning -import Categories.Object.Monoid as MonoidObject - -open import Categories.Category.Cocartesian using (module CocartesianMonoidal) -open import Categories.Category.Product using (_⁂_) -open import Categories.Functor.Monoidal using (MonoidalFunctor; IsMonoidalFunctor) -open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) -open import Categories.Morphism using (_≅_) -open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Data.Product using (_,_) - -module G = Functor G -module M = Functor M -module 𝒞-M = CocartesianMonoidal 𝒞.U 𝒞.cocartesian - -open 𝒞 using (⊥; -+-; _+_; _+₁_; i₁; i₂; inject₁; inject₂) -module +-assoc {n} {m} {o} = _≅_ (𝒞.+-assoc {n} {m} {o}) -module +-λ {n} = _≅_ (𝒞-M.⊥+A≅A {n}) -module +-ρ {n} = _≅_ (𝒞-M.A+⊥≅A {n}) - -module _ where - - open 𝒞 - open ⇒-Reasoning U - open ⊗-Reasoning 𝒞-M.+-monoidal - - module _ {n m o : Obj} where - - private - - +-α : (n + m) + o 𝒞.⇒ n + (m + o) - +-α = +-assoc.to {n} {m} {o} - - +-α∘i₂ : +-α ∘ i₂ ≈ i₂ ∘ i₂ - +-α∘i₂ = inject₂ - - +-α∘i₁∘i₁ : (+-α ∘ i₁) ∘ i₁ ≈ i₁ - +-α∘i₁∘i₁ = inject₁ ⟩∘⟨refl ○ inject₁ - - +-α∘i₁∘i₂ : (+-α ∘ i₁) ∘ i₂ ≈ i₂ ∘ i₁ - +-α∘i₁∘i₂ = inject₁ ⟩∘⟨refl ○ inject₂ - - module _ {n : Obj} where - - +-ρ∘i₁ : +-ρ.from {n} ∘ i₁ ≈ id - +-ρ∘i₁ = inject₁ - - +-λ∘i₂ : +-λ.from {n} ∘ i₂ ≈ id - +-λ∘i₂ = inject₂ - -open S -open Functor -open MonoidalFunctor -open MonoidObject S.monoidal using (Monoid; Monoid⇒) -open Monoid renaming (assoc to μ-assoc; identityˡ to μ-identityˡ; identityʳ to μ-identityʳ) -open Monoid⇒ - -Forget : Functor (Monoids monoidal) U -Forget .F₀ = Carrier -Forget .F₁ = arr -Forget .identity = Equiv.refl -Forget .homomorphism = Equiv.refl -Forget .F-resp-≈ x = x - -𝒞-MC : MonoidalCategory o ℓ e -𝒞-MC = record { monoidal = 𝒞-M.+-monoidal } - -List : Functor U U -List = Forget ∙ M - -module List = Functor List - -List∘G : Functor 𝒞.U U -List∘G = List ∙ G - -module LG = Functor List∘G - -[] : {A : Obj} → unit ⇒ List.₀ A -[] {A} = η (M.₀ A) - -++ : {A : Obj} → List.₀ A ⊗₀ List.₀ A ⇒ List.₀ A -++ {A} = μ (M.₀ A) - -++⇒ : {A B : Obj} (f : A ⇒ B) → List.₁ f ∘ ++ ≈ ++ ∘ List.₁ f ⊗₁ List.₁ f -++⇒ f = preserves-μ (M.₁ f) - -[]⇒ : {A B : Obj} (f : A ⇒ B) → List.₁ f ∘ [] ≈ [] -[]⇒ f = preserves-η (M.₁ f) - -++-⊗ : {n m : 𝒞.Obj} → LG.₀ n ⊗₀ LG.₀ m ⇒ LG.₀ (n + m) -++-⊗ = ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂ - -open ⇒-Reasoning U -open ⊗-Reasoning monoidal - -module _ {n n′ m m′ : 𝒞.Obj} (f : n 𝒞.⇒ n′) (g : m 𝒞.⇒ m′) where - - LG[+₁∘i₁] : LG.₁ (f +₁ g) ∘ LG.₁ i₁ ≈ LG.₁ i₁ ∘ LG.₁ f - LG[+₁∘i₁] = [ List∘G ]-resp-square inject₁ - - LG[+₁∘i₂] : LG.₁ (f +₁ g) ∘ LG.₁ i₂ ≈ LG.₁ i₂ ∘ LG.₁ g - LG[+₁∘i₂] = [ List∘G ]-resp-square inject₂ - - ++-⊗-commute : ++-⊗ ∘ LG.₁ f ⊗₁ LG.₁ g ≈ LG.₁ (f +₁ g) ∘ ++-⊗ - ++-⊗-commute = begin - (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ LG.₁ f ⊗₁ LG.₁ g ≈⟨ pushʳ (parallel LG[+₁∘i₁] LG[+₁∘i₂]) ⟨ - ++ ∘ (LG.₁ (f +₁ g) ⊗₁ LG.₁ (f +₁ g)) ∘ (LG.₁ i₁ ⊗₁ LG.₁ i₂) ≈⟨ extendʳ (++⇒ (G.₁ (f +₁ g))) ⟨ - LG.₁ (f +₁ g) ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂ ∎ - -open ⊗-Util.Shorthands monoidal - -++-homo : NaturalTransformation (⊗ ∙ (List∘G ⁂ List∘G)) (List∘G ∙ -+-) -++-homo = ntHelper record - { η = λ (n , m) → ++-⊗ {n} {m} - ; commute = λ { {n , m} {n′ , m′} (f , g) → ++-⊗-commute f g } - } - -α-++-⊗ - : {n m o : 𝒞.Obj} - → LG.₁ (+-assoc.to {n} {m} {o}) - ∘ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) - ∘ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ⊗₁ id - ≈ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) - ∘ id ⊗₁ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) - ∘ α⇒ -α-++-⊗ {n} {m} {o} = begin - LG.₁ +-α ∘ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ⊗₁ id ≈⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ - LG.₁ +-α ∘ ++ ∘ (LG.₁ i₁ ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ⊗₁ LG.₁ i₂ ≈⟨ extendʳ (++⇒ (G.₁ +-α)) ⟩ - ++ ∘ LG.₁ +-α ⊗₁ LG.₁ +-α ∘ (LG.₁ i₁ ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ⊗₁ LG.₁ i₂ ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ - ++ ∘ (LG.₁ +-α ∘ LG.₁ i₁ ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ⊗₁ (LG.₁ +-α ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ pullˡ (Equiv.sym LG.homomorphism) ⟩⊗⟨ [ List∘G ]-resp-square +-α∘i₂ ⟩ - ++ ∘ (LG.₁ (+-α 𝒞.∘ i₁) ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ extendʳ (++⇒ (G.₁ (+-α 𝒞.∘ i₁))) ⟩⊗⟨refl ⟩ - ++ ∘ (++ ∘ LG.₁ (+-α 𝒞.∘ i₁) ⊗₁ LG.₁ (+-α 𝒞.∘ i₁) ∘ _) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩⊗⟨refl ⟨ - ++ ∘ (++ ∘ _ ⊗₁ (LG.₁ (+-α 𝒞.∘ i₁) ∘ LG.₁ i₂)) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ [ List∘G ]-resp-∘ +-α∘i₁∘i₁ ⟩⊗⟨ [ List∘G ]-resp-square +-α∘i₁∘i₂) ⟩⊗⟨refl ⟩ - ++ ∘ (++ ∘ LG.₁ i₁ ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₁)) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ split₁ˡ ⟩ - ++ ∘ ++ ⊗₁ id ∘ (LG.₁ i₁ ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₁)) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂) ≈⟨ extendʳ (μ-assoc (M.₀ (G.₀ (n + (m + o))))) ⟩ - ++ ∘ (id ⊗₁ ++ ∘ α⇒) ∘ (LG.₁ i₁ ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₁)) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ assoc ⟩ - ++ ∘ id ⊗₁ ++ ∘ α⇒ ∘ (LG.₁ i₁ ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₁)) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟩ - ++ ∘ id ⊗₁ ++ ∘ LG.₁ i₁ ⊗₁ ((LG.₁ i₂ ∘ LG.₁ i₁) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂)) ∘ α⇒ ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - ++ ∘ LG.₁ i₁ ⊗₁ (++ ∘ (LG.₁ i₂ ∘ LG.₁ i₁) ⊗₁ (LG.₁ i₂ ∘ LG.₁ i₂)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩∘⟨refl ⟩ - ++ ∘ LG.₁ i₁ ⊗₁ (++ ∘ LG.₁ i₂ ⊗₁ LG.₁ i₂ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (extendʳ (++⇒ (G.₁ i₂))) ⟩∘⟨refl ⟨ - ++ ∘ LG.₁ i₁ ⊗₁ (LG.₁ i₂ ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ α⇒ ≈⟨ pushʳ (pushˡ split₂ʳ) ⟩ - (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ id ⊗₁ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ α⇒ ∎ - where - +-α : (n + m) + o 𝒞.⇒ n + (m + o) - +-α = +-assoc.to {n} {m} {o} - - -module _ {n : 𝒞.Obj} where - - ++-[]ʳ : {A B : Obj} (f : A ⇒ B) → ++ ∘ List.₁ f ⊗₁ [] ≈ List.₁ f ∘ ρ⇒ - ++-[]ʳ {A} {B} f = begin - ++ ∘ List.₁ f ⊗₁ [] ≈⟨ refl⟩∘⟨ serialize₂₁ ⟩ - ++ ∘ id ⊗₁ [] ∘ List.₁ f ⊗₁ id ≈⟨ pullˡ (Equiv.sym (μ-identityʳ (M.₀ B))) ⟩ - ρ⇒ ∘ List.₁ f ⊗₁ id ≈⟨ unitorʳ-commute-from ⟩ - List.₁ f ∘ ρ⇒ ∎ - - ++-[]ˡ : {A B : Obj} (f : A ⇒ B) → ++ ∘ [] ⊗₁ List.₁ f ≈ List.₁ f ∘ λ⇒ - ++-[]ˡ {A} {B} f = begin - ++ ∘ [] ⊗₁ List.₁ f ≈⟨ refl⟩∘⟨ serialize₁₂ ⟩ - ++ ∘ [] ⊗₁ id ∘ id ⊗₁ List.₁ f ≈⟨ pullˡ (Equiv.sym (μ-identityˡ (M.₀ B))) ⟩ - λ⇒ ∘ id ⊗₁ List.₁ f ≈⟨ unitorˡ-commute-from ⟩ - List.₁ f ∘ λ⇒ ∎ - - ++-⊗-λ - : LG.₁ +-λ.from ∘ (++ ∘ LG.₁ (i₁ {⊥} {n}) ⊗₁ LG.₁ i₂) ∘ [] ⊗₁ id - ≈ λ⇒ - ++-⊗-λ = begin - LG.₁ +-λ.from ∘ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ [] ⊗₁ id ≈⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ - LG.₁ +-λ.from ∘ ++ ∘ (LG.₁ i₁ ∘ []) ⊗₁ LG.₁ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []⇒ (G.₁ i₁) ⟩⊗⟨refl ⟩ - LG.₁ +-λ.from ∘ ++ ∘ [] ⊗₁ LG.₁ i₂ ≈⟨ refl⟩∘⟨ ++-[]ˡ (G.₁ i₂) ⟩ - LG.₁ +-λ.from ∘ LG.₁ i₂ ∘ λ⇒ ≈⟨ cancelˡ ([ List∘G ]-resp-∘ +-λ∘i₂ ○ LG.identity) ⟩ - λ⇒ ∎ - - ++-⊗-ρ - : LG.₁ +-ρ.from ∘ (++ ∘ LG.₁ (i₁ {n}) ⊗₁ LG.₁ i₂) ∘ id ⊗₁ [] - ≈ ρ⇒ - ++-⊗-ρ = begin - LG.₁ +-ρ.from ∘ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ id ⊗₁ [] ≈⟨ refl⟩∘⟨ pullʳ merge₂ʳ ⟩ - LG.₁ +-ρ.from ∘ ++ ∘ LG.₁ i₁ ⊗₁ (LG.₁ i₂ ∘ []) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ []⇒ (G.₁ i₂) ⟩ - LG.₁ +-ρ.from ∘ ++ ∘ LG.₁ i₁ ⊗₁ [] ≈⟨ refl⟩∘⟨ ++-[]ʳ (G.₁ i₁) ⟩ - LG.₁ +-ρ.from ∘ LG.₁ i₁ ∘ ρ⇒ ≈⟨ cancelˡ ([ List∘G ]-resp-∘ +-ρ∘i₁ ○ LG.identity) ⟩ - ρ⇒   ∎ - -open IsMonoidalFunctor - -ListOf,++,[] : MonoidalFunctor 𝒞-MC S -ListOf,++,[] .F = List∘G -ListOf,++,[] .isMonoidal .ε = [] -ListOf,++,[] .isMonoidal .⊗-homo = ++-homo -ListOf,++,[] .isMonoidal .associativity = α-++-⊗ -ListOf,++,[] .isMonoidal .unitaryˡ = ++-⊗-λ -ListOf,++,[] .isMonoidal .unitaryʳ = ++-⊗-ρ -- cgit v1.2.3