Generalize ListOf construction to arbitrary monoidmain

1 files changed, 110 insertions, 0 deletions

diff --git a/NaturalTransformation/Monoidal/Construction/FamilyOfMonoids.agda b/NaturalTransformation/Monoidal/Construction/FamilyOfMonoids.agda
new file mode 100644
index 0000000..d67c21a
--- /dev/null
+++ b/NaturalTransformation/Monoidal/Construction/FamilyOfMonoids.agda
@@ -0,0 +1,110 @@
+{-# 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 Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ˡ_)
+open import Level using (Level)
+
+-- A natural transformation between functors F, G
+-- from a cocartesian category 𝒞 to Monoids[S]
+-- can be turned into a monoidal natural transformation
+-- between monoidal functors F′ G′ from 𝒞 to S
+
+module NaturalTransformation.Monoidal.Construction.FamilyOfMonoids
+    {o o′ ℓ ℓ′ e e′ : Level}
+    {𝒞 : Category o ℓ e}
+    {𝒞-+ : Cocartesian 𝒞}
+    {S : MonoidalCategory o′ ℓ′ e′}
+    (let module S = MonoidalCategory S)
+    (M N : Functor 𝒞 (Monoids S.monoidal))
+    (α : NaturalTransformation M N)
+  where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Object.Monoid as MonoidObject
+import Functor.Monoidal.Construction.FamilyOfMonoids 𝒞-+ {S = S} as FamilyOfMonoids
+
+open import Categories.Category using (module Definitions)
+open import Categories.Functor.Properties using ([_]-resp-square)
+open import Categories.NaturalTransformation.Monoidal using (module Lax)
+open import Data.Product using (_,_)
+open import Functor.Forgetful.Instance.Monoid S using (Forget)
+
+private
+
+  module α = NaturalTransformation α
+  module M = Functor M
+  module N = Functor N
+  module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ })
+
+  open 𝒞 using (⊥; i₁; i₂; _+_)
+  open S
+
+  open MonoidObject monoidal using (Monoid; Monoid⇒)
+  open Definitions U using (CommutativeSquare)
+  open FamilyOfMonoids M using (F,⊗,ε)
+  open FamilyOfMonoids N using () renaming (F,⊗,ε to G,⊗,ε)
+  open Monoid using (μ; η)
+  open Monoid⇒
+  open ⇒-Reasoning U using (glue′)
+  open ⊗-Reasoning monoidal
+
+  F : Functor 𝒞 U
+  F = Forget ∙ M
+
+  G : Functor 𝒞 U
+  G = Forget ∙ N
+
+  β : NaturalTransformation F G
+  β = Forget ∘ˡ α
+
+  module F = Functor F
+  module G = Functor G
+  module β = NaturalTransformation β
+
+  module _ {A : 𝒞.Obj} where
+
+    εₘ : unit ⇒ F.₀ A
+    εₘ = η (M.₀ A)
+
+    ⊲ₘ : F.₀ A ⊗₀ F.₀ A ⇒ F.₀ A
+    ⊲ₘ = μ (M.₀ A)
+
+    εₙ : unit ⇒ G.₀ A
+    εₙ = η (N.₀ A)
+
+    ⊲ₙ : G.₀ A ⊗₀ G.₀ A ⇒ G.₀ A
+    ⊲ₙ = μ (N.₀ A)
+
+  ε-compat : β.η ⊥ ∘ εₘ ≈ εₙ
+  ε-compat = preserves-η (α.η ⊥)
+
+  module _ {n m : 𝒞.Obj} where
+
+    square : CommutativeSquare ⊲ₘ (β.η (n + m) ⊗₁ β.η (n + m)) (β.η (n + m)) ⊲ₙ
+    square = preserves-μ (α.η (n + m))
+
+    comm₁ : CommutativeSquare (F.₁ i₁) (β.η n) (β.η (n + m)) (G.₁ i₁)
+    comm₁ = β.commute i₁
+
+    comm₂ : CommutativeSquare (F.₁ i₂) (β.η m) (β.η (n + m)) (G.₁ i₂)
+    comm₂ = β.commute i₂
+
+    ⊗-homo-compat : CommutativeSquare (⊲ₘ ∘ F.₁ i₁ ⊗₁ F.₁ i₂) (β.η n ⊗₁ β.η m) (β.η (n + m)) (⊲ₙ ∘ G.₁ i₁ ⊗₁ G.₁ i₂)
+    ⊗-homo-compat = glue′ square (parallel comm₁ comm₂)
+
+open Lax.MonoidalNaturalTransformation hiding (ε-compat; ⊗-homo-compat)
+
+β,⊗,ε : Lax.MonoidalNaturalTransformation F,⊗,ε G,⊗,ε
+β,⊗,ε .U = β
+β,⊗,ε .isMonoidal = record
+    { ε-compat = ε-compat
+    ; ⊗-homo-compat = ⊗-homo-compat
+    }
+
+module β,⊗,ε = Lax.MonoidalNaturalTransformation β,⊗,ε