aboutsummaryrefslogtreecommitdiff
path: root/Functor/Monoidal/Construction
diff options
context:
space:
mode:
Diffstat (limited to 'Functor/Monoidal/Construction')
-rw-r--r--Functor/Monoidal/Construction/ListOf.agda213
1 files changed, 213 insertions, 0 deletions
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Κ³ = ++-βŠ—-ρ
generated by cgit v1.2.3 (git 2.39.1) at 2025-11-29 08:03:14 +0000