diff options
Diffstat (limited to 'Functor/Monoidal/Construction/ListOf.agda')
| -rw-r--r-- | Functor/Monoidal/Construction/ListOf.agda | 213 |
1 files changed, 0 insertions, 213 deletions
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ʳ = ++-⊗-ρ |