From e70481cf98eeb00154536e364dec58e79b034cc5 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 5 Nov 2025 00:09:51 -0600
Subject: Add list-of construction for monoidal functors

If F is a functor from a cocartesian category into Set, then the functor
taking n to List (F n) can be made into a monoidal functor.

More generally, Set can be replaced with any monoidal category D that
has a free monoid functor Free : D -> Monoids[D]
---
 Functor/Monoidal/Construction/ListOf.agda | 213 ++++++++++++++++++++++++++++++
 1 file changed, 213 insertions(+)
 create mode 100644 Functor/Monoidal/Construction/ListOf.agda

(limited to 'Functor')

diff --git a/Functor/Monoidal/Construction/ListOf.agda b/Functor/Monoidal/Construction/ListOf.agda
new file mode 100644
index 0000000..476939e
--- /dev/null
+++ b/Functor/Monoidal/Construction/ListOf.agda
@@ -0,0 +1,213 @@
+{-# 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 ℓ 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