1 files changed, 214 insertions, 0 deletions

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,⊗,ε