aboutsummaryrefslogtreecommitdiff
path: root/Functor/Monoidal
diff options
context:
space:
mode:
Diffstat (limited to 'Functor/Monoidal')
-rw-r--r--Functor/Monoidal/Braided/Strong/Properties.agda59
-rw-r--r--Functor/Monoidal/Construction/MonoidValued.agda214
-rw-r--r--Functor/Monoidal/Construction/MultisetOf.agda89
-rw-r--r--Functor/Monoidal/Instance/Nat/Circ.agda87
-rw-r--r--Functor/Monoidal/Instance/Nat/Preimage.agda164
-rw-r--r--Functor/Monoidal/Instance/Nat/Pull.agda166
-rw-r--r--Functor/Monoidal/Instance/Nat/Push.agda209
-rw-r--r--Functor/Monoidal/Instance/Nat/System.agda394
-rw-r--r--Functor/Monoidal/Strong/Properties.agda104
9 files changed, 1486 insertions, 0 deletions
diff --git a/Functor/Monoidal/Braided/Strong/Properties.agda b/Functor/Monoidal/Braided/Strong/Properties.agda
new file mode 100644
index 0000000..66dc4c0
--- /dev/null
+++ b/Functor/Monoidal/Braided/Strong/Properties.agda
@@ -0,0 +1,59 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+open import Categories.Category.Monoidal using (BraidedMonoidalCategory)
+open import Categories.Functor.Monoidal.Braided using (module Strong)
+open Strong using (BraidedMonoidalFunctor)
+
+module Functor.Monoidal.Braided.Strong.Properties
+ {o o′ ℓ ℓ′ e e′ : Level}
+ {C : BraidedMonoidalCategory o ℓ e}
+ {D : BraidedMonoidalCategory o′ ℓ′ e′}
+ (F,φ,ε : BraidedMonoidalFunctor C D) where
+
+import Categories.Category.Construction.Core as Core
+import Categories.Category.Monoidal.Utilities as ⊗-Utilities
+import Functor.Monoidal.Strong.Properties as MonoidalProp
+
+open import Categories.Functor.Properties using ([_]-resp-≅)
+
+private
+
+ module C = BraidedMonoidalCategory C
+ module D = BraidedMonoidalCategory D
+
+open D
+open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ)
+open ⊗-Utilities monoidal using (_⊗ᵢ_)
+open BraidedMonoidalFunctor F,φ,ε
+open MonoidalProp monoidalFunctor public
+
+private
+
+ variable
+ A B : Obj
+ X Y : C.Obj
+
+ σ : A ⊗₀ B ≅ B ⊗₀ A
+ σ = braiding.FX≅GX
+
+ σ⇐ : B ⊗₀ A ⇒ A ⊗₀ B
+ σ⇐ = braiding.⇐.η _
+
+ Fσ : F₀ (X C.⊗₀ Y) ≅ F₀ (Y C.⊗₀ X)
+ Fσ = [ F ]-resp-≅ C.braiding.FX≅GX
+
+ Fσ⇐ : F₀ (Y C.⊗₀ X) ⇒ F₀ (X C.⊗₀ Y)
+ Fσ⇐ = F₁ (C.braiding.⇐.η _)
+
+ φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y)
+ φ = ⊗-homo.FX≅GX
+
+open HomReasoning
+open Shorthands using (φ⇐)
+
+braiding-compatᵢ : Fσ {X} {Y} ∘ᵢ φ ≈ᵢ φ ∘ᵢ σ
+braiding-compatᵢ = ⌞ braiding-compat ⌟
+
+braiding-compat-inv : φ⇐ ∘ Fσ⇐ {X} {Y} ≈ σ⇐ ∘ φ⇐
+braiding-compat-inv = to-≈ braiding-compatᵢ
diff --git a/Functor/Monoidal/Construction/MonoidValued.agda b/Functor/Monoidal/Construction/MonoidValued.agda
new file mode 100644
index 0000000..937714d
--- /dev/null
+++ b/Functor/Monoidal/Construction/MonoidValued.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.MonoidValued
+ {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.monoidal 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,⊗,ε
diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda
new file mode 100644
index 0000000..83bdf52
--- /dev/null
+++ b/Functor/Monoidal/Construction/MultisetOf.agda
@@ -0,0 +1,89 @@
+{-# 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 (SymmetricMonoidalCategory)
+open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
+open import Category.Construction.CMonoids using (CMonoids)
+
+open import Level using (Level)
+
+module Functor.Monoidal.Construction.MultisetOf
+ {o o′ ℓ ℓ′ e e′ : Level}
+ {𝒞 : CocartesianCategory o ℓ e}
+ {S : SymmetricMonoidalCategory o′ ℓ′ e′}
+ (let module 𝒞 = CocartesianCategory 𝒞)
+ (let module S = SymmetricMonoidalCategory S)
+ (G : Functor 𝒞.U S.U)
+ (M : Functor S.U (CMonoids S.symmetric))
+ where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Category.Monoidal.Utilities as ⊗-Util
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Object.Monoid.Commutative as CMonoidObject
+
+open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
+open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands)
+open import Categories.Functor.Monoidal using (MonoidalFunctor)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Categories.Functor.Properties using ([_]-resp-∘)
+open import Data.Product using (_,_)
+
+module G = Functor G
+module M = Functor M
+module 𝒞-SM = CocartesianSymmetricMonoidal 𝒞.U 𝒞.cocartesian
+
+open 𝒞 using (⊥; -+-; _+_; _+₁_; i₁; i₂; inject₁; inject₂; +-swap)
+open Lax using (SymmetricMonoidalFunctor)
+
+open S
+open Functor
+open CMonoidObject symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
+open CommutativeMonoid renaming (assoc to μ-assoc; identityˡ to μ-identityˡ; identityʳ to μ-identityʳ; commutative to μ-commutative)
+open CommutativeMonoid⇒
+
+Forget : Functor (CMonoids symmetric) (Monoids monoidal)
+Forget .F₀ = monoid
+Forget .F₁ = monoid⇒
+Forget .identity = Equiv.refl
+Forget .homomorphism = Equiv.refl
+Forget .F-resp-≈ x = x
+
+𝒞-SMC : SymmetricMonoidalCategory o ℓ e
+𝒞-SMC = record { symmetric = 𝒞-SM.+-symmetric }
+
+open import Functor.Monoidal.Construction.ListOf {𝒞 = 𝒞} G (Forget ∙ M)
+ using (List∘G; ListOf,++,[]; module LG; ++; module List; ++⇒)
+
+open Shorthands symmetric
+
+++-swap : {A : Obj} → ++ {A} ≈ ++ ∘ σ⇒
+++-swap {A} = μ-commutative (M.₀ A)
+
+open ⇒-Reasoning U
+open ⊗-Reasoning monoidal
+
+++-⊗-σ
+ : {X Y : 𝒞.Obj}
+ → LG.₁ (+-swap {X} {Y}) ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂
+ ≈ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ σ⇒
+++-⊗-σ {X} {Y} = begin
+ LG.₁ +-swap ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂ ≈⟨ extendʳ (++⇒ (G.₁ +-swap)) ⟩
+ ++ ∘ LG.₁ +-swap ⊗₁ LG.₁ +-swap ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂ ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨
+ ++ ∘ (LG.₁ +-swap ∘ LG.₁ i₁) ⊗₁ (LG.₁ +-swap ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ [ List∘G ]-resp-∘ inject₁ ⟩⊗⟨ [ List∘G ]-resp-∘ inject₂ ⟩
+ ++ ∘ LG.₁ i₂ ⊗₁ LG.₁ i₁ ≈⟨ pushˡ ++-swap ⟩
+ ++ ∘ σ⇒ ∘ LG.₁ i₂ ⊗₁ LG.₁ i₁ ≈⟨ pushʳ (braiding.⇒.commute (LG.₁ i₂ , LG.₁ i₁ )) ⟩
+ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ σ⇒ ∎
+
+open SymmetricMonoidalFunctor
+
+module ListOf,++,[] = MonoidalFunctor ListOf,++,[]
+
+MultisetOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S
+MultisetOf,++,[] .F = List∘G
+MultisetOf,++,[] .isBraidedMonoidal = record
+ { isMonoidal = ListOf,++,[].isMonoidal
+ ; braiding-compat = ++-⊗-σ
+ }
diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda
new file mode 100644
index 0000000..1b45a75
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Circ.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; 0ℓ; suc)
+
+module Functor.Monoidal.Instance.Nat.Circ where
+
+import Categories.Object.Monoid as MonoidObject
+import Data.Permutation.Sort as ↭-Sort
+import Function.Reasoning as →-Reasoning
+
+open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+open import Category.Monoidal.Instance.Nat using (Nat,+,0)
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Categories.Category.Cartesian using (Cartesian)
+open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
+open import Categories.Functor using (_∘F_)
+open BinaryProducts products using (-×-)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Categories.Functor using (Functor)
+open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Data.Circuit using (Circuit; Circuitₛ; mkCircuit; mkCircuitₛ; _≈_; mk≈; map)
+open import Data.Circuit.Gate using (Gates)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Function using (_⟶ₛ_; Func; _⟨$⟩_; _∘_; id)
+open import Functor.Instance.Nat.Circ {suc 0ℓ} using (Circ; module Multiset∘Edge)
+open import Functor.Instance.Nat.Edge {suc 0ℓ} using (Edge)
+open import Function.Construct.Setoid using (_∙_)
+
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+
+open import Functor.Instance.FreeCMonoid {suc 0ℓ} {suc 0ℓ} using (FreeCMonoid)
+
+Nat-Cocartesian-Category : CocartesianCategory 0ℓ 0ℓ 0ℓ
+Nat-Cocartesian-Category = record { cocartesian = Nat-Cocartesian }
+
+open import Functor.Monoidal.Construction.MultisetOf
+ {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (MultisetOf,++,[])
+
+open Lax using (SymmetricMonoidalFunctor)
+
+module MultisetOf,++,[] = SymmetricMonoidalFunctor MultisetOf,++,[]
+
+open SymmetricMonoidalFunctor
+
+ε⇒ : ⊤ₛ ⟶ₛ Circuitₛ 0
+ε⇒ = mkCircuitₛ ∙ MultisetOf,++,[].ε
+
+open Cocartesian Nat-Cocartesian using (-+-)
+
+open Func
+
+η : {n m : ℕ} → Circuitₛ n ×ₛ Circuitₛ m ⟶ₛ Circuitₛ (n + m)
+η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (MultisetOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y))
+η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (MultisetOf,++,[].⊗-homo.η (n , m)) (x , y))
+
+⊗-homomorphism : NaturalTransformation (-×- ∘F (Circ ⁂ Circ)) (Circ ∘F -+-)
+⊗-homomorphism = ntHelper record
+ { η = λ (n , m) → η {n} {m}
+ ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (MultisetOf,++,[].⊗-homo.commute (f , g) {X , Y}) }
+ }
+
+Circ,⊗,ε : SymmetricMonoidalFunctor Nat,+,0 Setoids-×
+Circ,⊗,ε .F = Circ
+Circ,⊗,ε .isBraidedMonoidal = record
+ { isMonoidal = record
+ { ε = ε⇒
+ ; ⊗-homo = ⊗-homomorphism
+ ; associativity = λ { {n} {m} {o} {(mkCircuit x , mkCircuit y) , mkCircuit z} →
+ mk≈ (MultisetOf,++,[].associativity {n} {m} {o} {(x , y) , z}) }
+ ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (MultisetOf,++,[].unitaryˡ {n} {_ , x}) }
+ ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (MultisetOf,++,[].unitaryʳ {n} {x , _}) }
+ }
+ ; braiding-compat = λ { {n} {m} {mkCircuit x , mkCircuit y} →
+ mk≈ (MultisetOf,++,[].braiding-compat {n} {m} {x , y}) }
+ }
diff --git a/Functor/Monoidal/Instance/Nat/Preimage.agda b/Functor/Monoidal/Instance/Nat/Preimage.agda
new file mode 100644
index 0000000..844df79
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Preimage.agda
@@ -0,0 +1,164 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Monoidal.Instance.Nat.Preimage where
+
+open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Functor using (_∘F_)
+open import Data.Subset.Functional using (Subset)
+open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Product.Base using (_,_; _×_; Σ)
+open import Data.Vec.Functional using ([]; _++_)
+open import Data.Vec.Functional.Properties using (++-cong)
+open import Data.Vec.Functional using (Vector; [])
+open import Function.Bundles using (Func; _⟶ₛ_)
+open import Functor.Instance.Nat.Preimage using (Preimage; Subsetₛ)
+open import Level using (0ℓ)
+
+open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+open BinaryProducts products using (-×-)
+open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-swap; +₁∘+-swap)
+open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
+
+open import Data.Fin.Base using (Fin; splitAt; join; _↑ˡ_; _↑ʳ_)
+open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ)
+open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂)
+open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘)
+open import Data.Fin.Preimage using (preimage)
+open import Function.Base using (_∘_; id)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
+open import Data.Bool.Base using (Bool)
+
+open Func
+Preimage-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Subsetₛ 0
+to Preimage-ε x = []
+cong Preimage-ε x ()
+
+++ₛ : {n m : ℕ} → Subsetₛ n ×ₛ Subsetₛ m ⟶ₛ Subsetₛ (n + m)
+to ++ₛ (xs , ys) = xs ++ ys
+cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
+
+preimage-++
+ : {n n′ m m′ : ℕ}
+ (f : Fin n → Fin n′)
+ (g : Fin m → Fin m′)
+ {xs : Subset n′}
+ {ys : Subset m′}
+ → preimage f xs ++ preimage g ys ≗ preimage (f +₁ g) (xs ++ ys)
+preimage-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin
+ (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨
+ [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨
+ [ xs , ys ]′ (splitAt n′ (join n′ m′ (map f g (splitAt n e)))) ≡⟨ ≡.cong ([ xs , ys ]′ ∘ splitAt n′) ([,]-map (splitAt n e)) ⟩
+ [ xs , ys ]′ (splitAt n′ ((f +₁ g) e)) ∎
+ where
+ open ≡-Reasoning
+
+⊗-homomorphism : NaturalTransformation (-×- ∘F (Preimage ⁂ Preimage)) (Preimage ∘F -+-)
+⊗-homomorphism = ntHelper record
+ { η = λ (n , m) → ++ₛ {n} {m}
+ ; commute = λ { {n′ , m′} {n , m} (f , g) {xs , ys} e → preimage-++ f g e }
+ }
+
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Lax)
+open Lax using (SymmetricMonoidalFunctor)
+
+++-assoc
+ : {m n o : ℕ}
+ (X : Subset m)
+ (Y : Subset n)
+ (Z : Subset o)
+ → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z)
+++-assoc {m} {n} {o} X Y Z i = begin
+ ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩
+ [ [ X , Y ]′ ∘ splitAt m , Z ]′ (splitAt (m + n) (+-assocʳ {m} i)) ≡⟨ [,]-cong ([,]-cong (inv ∘ X) (inv ∘ Y) ∘ splitAt m) (inv ∘ Z) (splitAt (m + n) (+-assocʳ {m} i)) ⟨
+ [ [ b ∘ X′ , b ∘ Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [-,]-cong ([,]-∘ b ∘ splitAt m) (splitAt (m + n) (+-assocʳ {m} i)) ⟨
+ [ b ∘ [ X′ , Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [,]-∘ b (splitAt (m + n) (+-assocʳ {m} i)) ⟨
+ b ([ [ X′ , Y′ ]′ ∘ splitAt m , Z′ ]′ (splitAt _ (+-assocʳ {m} i))) ≡⟨ ≡.cong b ([]∘assocʳ {2} {m} i) ⟩
+ b ([ X′ , [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩
+ [ b ∘ X′ , b ∘ [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ b ∘ splitAt n) (splitAt m i) ⟩
+ [ b ∘ X′ , [ b ∘ Y′ , b ∘ Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ X) ([,]-cong (inv ∘ Y) (inv ∘ Z) ∘ splitAt n) (splitAt m i) ⟩
+ [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩
+ (X ++ (Y ++ Z)) i ∎
+ where
+ open Bool
+ open Fin
+ f : Bool → Fin 2
+ f false = zero
+ f true = suc zero
+ b : Fin 2 → Bool
+ b zero = false
+ b (suc zero) = true
+ inv : b ∘ f ≗ id
+ inv false = ≡.refl
+ inv true = ≡.refl
+ X′ : Fin m → Fin 2
+ X′ = f ∘ X
+ Y′ : Fin n → Fin 2
+ Y′ = f ∘ Y
+ Z′ : Fin o → Fin 2
+ Z′ = f ∘ Z
+ open ≡-Reasoning
+
+Preimage-unitaryˡ
+ : {n : ℕ}
+ (X : Subset n)
+ → (X ++ []) ∘ (_↑ˡ 0) ≗ X
+Preimage-unitaryˡ {n} X i = begin
+ [ X , [] ]′ (splitAt _ (i ↑ˡ 0)) ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩
+ [ X , [] ]′ (inj₁ i) ≡⟨⟩
+ X i ∎
+ where
+ open ≡-Reasoning
+
+++-swap
+ : {n m : ℕ}
+ (X : Subset n)
+ (Y : Subset m)
+ → (X ++ Y) ∘ +-swap {n} ≗ Y ++ X
+++-swap {n} {m} X Y i = begin
+ [ X , Y ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-cong (inv ∘ X) (inv ∘ Y) (splitAt n (+-swap {n} i)) ⟨
+ [ b ∘ X′ , b ∘ Y′ ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-∘ b (splitAt n (+-swap {n} i)) ⟨
+ b ([ X′ , Y′ ]′ (splitAt n (+-swap {n} i))) ≡⟨ ≡.cong b ([]∘swap {2} {n} i) ⟩
+ b ([ Y′ , X′ ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩
+ [ b ∘ Y′ , b ∘ X′ ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ Y) (inv ∘ X) (splitAt m i) ⟩
+ [ Y , X ]′ (splitAt m i) ∎
+ where
+ open Bool
+ open Fin
+ f : Bool → Fin 2
+ f false = zero
+ f true = suc zero
+ b : Fin 2 → Bool
+ b zero = false
+ b (suc zero) = true
+ inv : b ∘ f ≗ id
+ inv false = ≡.refl
+ inv true = ≡.refl
+ X′ : Fin n → Fin 2
+ X′ = f ∘ X
+ Y′ : Fin m → Fin 2
+ Y′ = f ∘ Y
+ open ≡-Reasoning
+
+open SymmetricMonoidalFunctor
+Preimage,++,[] : SymmetricMonoidalFunctor
+Preimage,++,[] .F = Preimage
+Preimage,++,[] .isBraidedMonoidal = record
+ { isMonoidal = record
+ { ε = Preimage-ε
+ ; ⊗-homo = ⊗-homomorphism
+ ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i }
+ ; unitaryˡ = λ _ → ≡.refl
+ ; unitaryʳ = λ { {n} {X , _} i → Preimage-unitaryˡ X i }
+ }
+ ; braiding-compat = λ { {n} {m} {X , Y} i → ++-swap X Y i }
+ }
diff --git a/Functor/Monoidal/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda
new file mode 100644
index 0000000..b267f97
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Pull.agda
@@ -0,0 +1,166 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Monoidal.Instance.Nat.Pull where
+
+import Categories.Morphism as Morphism
+
+open import Level using (0ℓ; Level)
+
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian)
+
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Functor using (_∘F_)
+open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Strong)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Vector using (++-assoc)
+open import Data.Fin.Base using (Fin; splitAt; join)
+open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
+open import Data.Fin.Preimage using (preimage)
+open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ; splitAt-↑ʳ; join-splitAt)
+open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Product.Base using (_,_; _×_; Σ; proj₁; proj₂)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (∣_∣)
+open import Data.Subset.Functional using (Subset)
+open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂)
+open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘)
+open import Data.System.Values Monoid using (Values; <ε>; []-unique; _++_; ++ₛ; splitₛ; _≋_; [])
+open import Data.Unit.Polymorphic using (tt)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Functor.Instance.Nat.Pull using (Pull; Pull-defs)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
+
+open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+
+open BinaryProducts products using (-×-)
+open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-comm; +-swap; +₁∘+-swap; i₁; i₂)
+open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
+open Func
+open Morphism (Setoids-×.U) using (_≅_; module Iso)
+open Strong using (SymmetricMonoidalFunctor)
+open ≡-Reasoning
+
+private
+
+ open _≅_
+ open Iso
+
+ Pull-ε : ⊤ₛ ≅ Values 0
+ from Pull-ε = Const ⊤ₛ (Values 0) []
+ to Pull-ε = Const (Values 0) ⊤ₛ tt
+ isoˡ (iso Pull-ε) = tt
+ isoʳ (iso Pull-ε) {x} = []-unique [] x
+
+ opaque
+ unfolding _++_
+ unfolding Pull-defs
+ Pull-++
+ : {n n′ m m′ : ℕ}
+ (f : Fin n → Fin n′)
+ (g : Fin m → Fin m′)
+ {xs : ∣ Values n′ ∣}
+ {ys : ∣ Values m′ ∣}
+ → (Pull.₁ f ⟨$⟩ xs) ++ (Pull.₁ g ⟨$⟩ ys) ≋ Pull.₁ (f +₁ g) ⟨$⟩ (xs ++ ys)
+ Pull-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin
+ (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨
+ [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨
+ (xs ++ ys) (join n′ m′ (map f g (splitAt n e))) ≡⟨ ≡.cong (xs ++ ys) ([,]-map (splitAt n e)) ⟩
+ (xs ++ ys) ((f +₁ g) e) ∎
+
+ module _ {n m : ℕ} where
+
+ opaque
+ unfolding splitₛ
+
+ open import Function.Construct.Setoid using (setoid)
+ open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_)
+ open import Function.Construct.Setoid using (_∙_)
+ open import Function.Construct.Identity using () renaming (function to Id)
+
+ split∘++ : splitₛ ∙ ++ₛ ≈ Id (Values n ×ₛ Values m)
+ split∘++ {xs , ys} .proj₁ i = ≡.cong [ xs , ys ]′ (splitAt-↑ˡ n i m)
+ split∘++ {xs , ys} .proj₂ i = ≡.cong [ xs , ys ]′ (splitAt-↑ʳ n m i)
+
+ ++∘split : ++ₛ {n} ∙ splitₛ ≈ Id (Values (n + m))
+ ++∘split {x} i = ≡.trans (≡.sym ([,]-∘ x (splitAt n i))) (≡.cong x (join-splitAt n m i))
+
+ ⊗-homomorphism : NaturalIsomorphism (-×- ∘F (Pull ⁂ Pull)) (Pull ∘F -+-)
+ ⊗-homomorphism = niHelper record
+ { η = λ (n , m) → ++ₛ {n} {m}
+ ; η⁻¹ = λ (n , m) → splitₛ {n} {m}
+ ; commute = λ { {n , m} {n′ , m′} (f , g) {xs , ys} → Pull-++ f g }
+ ; iso = λ (n , m) → record
+ { isoˡ = split∘++
+ ; isoʳ = ++∘split
+ }
+ }
+
+ module _ {n m : ℕ} where
+
+ opaque
+ unfolding Pull-++
+
+ Pull-i₁
+ : (X : ∣ Values n ∣)
+ (Y : ∣ Values m ∣)
+ → Pull.₁ i₁ ⟨$⟩ (X ++ Y) ≋ X
+ Pull-i₁ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m)
+
+ Pull-i₂
+ : (X : ∣ Values n ∣)
+ (Y : ∣ Values m ∣)
+ → Pull.₁ i₂ ⟨$⟩ (X ++ Y) ≋ Y
+ Pull-i₂ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i)
+
+ opaque
+ unfolding Pull-++
+
+ Push-assoc
+ : {m n o : ℕ}
+ (X : ∣ Values m ∣)
+ (Y : ∣ Values n ∣)
+ (Z : ∣ Values o ∣)
+ → Pull.₁ (+-assocʳ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z) ≋ X ++ (Y ++ Z)
+ Push-assoc {m} {n} {o} X Y Z i = ++-assoc X Y Z i
+
+ Pull-swap
+ : {n m : ℕ}
+ (X : ∣ Values n ∣)
+ (Y : ∣ Values m ∣)
+ → Pull.₁ (+-swap {n}) ⟨$⟩ (X ++ Y) ≋ Y ++ X
+ Pull-swap {n} {m} X Y i = begin
+ ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
+ [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (Pull-i₂ X Y) (splitAt m i) ⟩
+ [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (Pull-i₁ X Y) (splitAt m i) ⟩
+ [ Y , X ]′ (splitAt m i) ≡⟨⟩
+ (Y ++ X) i ∎
+
+open SymmetricMonoidalFunctor
+
+Pull,++,[] : SymmetricMonoidalFunctor
+Pull,++,[] .F = Pull
+Pull,++,[] .isBraidedMonoidal = record
+ { isStrongMonoidal = record
+ { ε = Pull-ε
+ ; ⊗-homo = ⊗-homomorphism
+ ; associativity = λ { {_} {_} {_} {(X , Y) , Z} → Push-assoc X Y Z }
+ ; unitaryˡ = λ { {n} {_ , X} → Pull-i₂ {0} {n} [] X }
+ ; unitaryʳ = λ { {n} {X , _} → Pull-i₁ {n} {0} X [] }
+ }
+ ; braiding-compat = λ { {n} {m} {X , Y} → Pull-swap X Y }
+ }
+
+module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda
new file mode 100644
index 0000000..2e8c0cf
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Push.agda
@@ -0,0 +1,209 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Monoidal.Instance.Nat.Push where
+
+open import Categories.Category.Instance.Nat using (Nat)
+open import Data.Bool.Base using (Bool; false)
+open import Data.Subset.Functional using (Subset; ⁅_⁆; ⊥)
+open import Function.Base using (_∘_; case_of_; _$_; id)
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Level using (0ℓ; Level)
+open import Relation.Binary using (Rel; Setoid)
+open import Functor.Instance.Nat.Push using (Push; Push-defs)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Data.Vec.Functional as Vec using (Vector)
+open import Data.Vector using (++-assoc; ++-↑ˡ; ++-↑ʳ)
+-- open import Data.Vec.Functional.Properties using (++-cong)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Functor using () renaming (_∘F_ to _∘′_)
+open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assoc; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Fin using (Fin)
+open import Data.Product.Base using (_,_; _×_; Σ)
+open import Data.Fin.Preimage using (preimage; preimage-⊥; preimage-cong₂)
+open import Functor.Monoidal.Instance.Nat.Preimage using (preimage-++)
+open import Data.Sum.Base using ([_,_]; [_,_]′; inj₁; inj₂)
+open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map)
+open import Data.Circuit.Merge using (merge-with; merge; merge-⊥; merge-[]; ⁅⁆-++; merge-++; merge-cong₁; merge-cong₂; merge-suc; _when_; join-merge; merge-preimage-ρ; merge-⁅⁆)
+open import Data.Circuit.Value using (Value; join; join-comm; join-assoc; Monoid)
+open import Data.Fin.Base using (splitAt; _↑ˡ_; _↑ʳ_) renaming (join to joinAt)
+open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; ↑ˡ-injective; ↑ʳ-injective; _≟_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning)
+open BinaryProducts products using (-×-)
+open Value using (U)
+open Bool using (false)
+
+open import Function.Bundles using (Equivalence)
+open import Category.Monoidal.Instance.Nat using (Nat,+,0)
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
+open Lax using (SymmetricMonoidalFunctor)
+open import Categories.Morphism Nat using (_≅_)
+open import Function.Bundles using (Inverse)
+open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
+open Dual.op-binaryProducts using () renaming (assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
+open import Relation.Nullary.Decidable using (does; does-⇔; dec-false)
+open import Data.Setoid using (∣_∣)
+
+open ℕ
+
+open import Data.System.Values Monoid using (Values; <ε>; ++ₛ; _++_; head; tail; _≋_)
+
+open Func
+open ≡-Reasoning
+
+private
+
+ Push-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Values 0
+ Push-ε = Const ⊤ₛ (Values 0) <ε>
+
+ opaque
+
+ unfolding _++_
+
+ unfolding Push-defs
+ Push-++
+ : {n n′ m m′ : ℕ }
+ → (f : Fin n → Fin n′)
+ → (g : Fin m → Fin m′)
+ → (xs : ∣ Values n ∣)
+ → (ys : ∣ Values m ∣)
+ → (Push.₁ f ⟨$⟩ xs) ++ (Push.₁ g ⟨$⟩ ys)
+ ≋ Push.₁ (f +₁ g) ⟨$⟩ (xs ++ ys)
+ Push-++ {n} {n′} {m} {m′} f g xs ys i = begin
+ ((merge xs ∘ preimage f ∘ ⁅_⁆) ++ (merge ys ∘ preimage g ∘ ⁅_⁆)) i
+ ≡⟨ [,]-cong left right (splitAt n′ i) ⟩
+ [ (λ x → merge (xs ++ ys) _) , (λ x → merge (xs ++ ys) _) ]′ (splitAt n′ i)
+ ≡⟨ [,]-∘ (merge (xs ++ ys) ∘ (preimage (f +₁ g))) (splitAt n′ i) ⟨
+ merge (xs ++ ys) (preimage (f +₁ g) ((⁅⁆++⊥ Vec.++ ⊥++⁅⁆) i)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-cong₂ (f +₁ g) (⁅⁆-++ {n′} i)) ⟩
+ merge (xs ++ ys) (preimage (f +₁ g) ⁅ i ⁆) ∎
+ where
+ ⁅⁆++⊥ : Vector (Subset (n′ + m′)) n′
+ ⁅⁆++⊥ x = ⁅ x ⁆ Vec.++ ⊥
+ ⊥++⁅⁆ : Vector (Subset (n′ + m′)) m′
+ ⊥++⁅⁆ x = ⊥ Vec.++ ⁅ x ⁆
+ left : (x : Fin n′) → merge xs (preimage f ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥))
+ left x = begin
+ merge xs (preimage f ⁅ x ⁆) ≡⟨ join-comm U (merge xs (preimage f ⁅ x ⁆)) ⟩
+ join (merge xs (preimage f ⁅ x ⁆)) U ≡⟨ ≡.cong (join (merge _ _)) (merge-⊥ ys) ⟨
+ join (merge xs (preimage f ⁅ x ⁆)) (merge ys ⊥) ≡⟨ ≡.cong (join (merge _ _)) (merge-cong₂ ys (preimage-⊥ g)) ⟨
+ join (merge xs (preimage f ⁅ x ⁆)) (merge ys (preimage g ⊥)) ≡⟨ merge-++ xs ys (preimage f ⁅ x ⁆) (preimage g ⊥) ⟨
+ merge (xs ++ ys) ((preimage f ⁅ x ⁆) Vec.++ (preimage g ⊥)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
+ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥)) ∎
+ right : (x : Fin m′) → merge ys (preimage g ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆))
+ right x = begin
+ merge ys (preimage g ⁅ x ⁆) ≡⟨⟩
+ join U (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-⊥ xs) ⟨
+ join (merge xs ⊥) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-cong₂ xs (preimage-⊥ f)) ⟨
+ join (merge xs (preimage f ⊥)) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ merge-++ xs ys (preimage f ⊥) (preimage g ⁅ x ⁆) ⟨
+ merge (xs ++ ys) ((preimage f ⊥) Vec.++ (preimage g ⁅ x ⁆)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
+ merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆)) ∎
+
+ ⊗-homomorphism : NaturalTransformation (-×- ∘′ (Push ⁂ Push)) (Push ∘′ -+-)
+ ⊗-homomorphism = ntHelper record
+ { η = λ (n , m) → ++ₛ {n} {m}
+ ; commute = λ { (f , g) {xs , ys} → Push-++ f g xs ys }
+ }
+
+ opaque
+
+ unfolding Push-defs
+ unfolding _++_
+
+ Push-assoc
+ : {m n o : ℕ}
+ (X : ∣ Values m ∣)
+ (Y : ∣ Values n ∣)
+ (Z : ∣ Values o ∣)
+ → (Push.₁ (+-assocˡ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z)) ≋ X ++ Y ++ Z
+ Push-assoc {m} {n} {o} X Y Z i = begin
+ merge ((X ++ Y) ++ Z) (preimage (+-assocˡ {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ ↔-mno ((X ++ Y) ++ Z) ⁅ i ⁆ ⟩
+ merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (⁅ i ⁆) ≡⟨⟩
+ merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (preimage id ⁅ i ⁆) ≡⟨ merge-cong₁ (++-assoc X Y Z) (preimage id ⁅ i ⁆) ⟩
+ merge (X ++ (Y ++ Z)) (preimage id ⁅ i ⁆) ≡⟨ Push.identity i ⟩
+ (X ++ (Y ++ Z)) i ∎
+ where
+ open Inverse
+ module +-assoc = _≅_ (+-assoc {m} {n} {o})
+ ↔-mno : Permutation ((m + n) + o) (m + (n + o))
+ ↔-mno .to = +-assocˡ {m}
+ ↔-mno .from = +-assocʳ {m}
+ ↔-mno .to-cong ≡.refl = ≡.refl
+ ↔-mno .from-cong ≡.refl = ≡.refl
+ ↔-mno .inverse = (λ { ≡.refl → +-assoc.isoˡ _ }) , λ { ≡.refl → +-assoc.isoʳ _ }
+
+ Push-unitaryˡ
+ : {n : ℕ}
+ (X : ∣ Values n ∣)
+ → Push.₁ id ⟨$⟩ (<ε> ++ X) ≋ X
+ Push-unitaryˡ = merge-⁅⁆
+
+ preimage-++′
+ : {n m o : ℕ}
+ (f : Vector (Fin o) n)
+ (g : Vector (Fin o) m)
+ (S : Subset o)
+ → preimage (f Vec.++ g) S ≗ preimage f S Vec.++ preimage g S
+ preimage-++′ {n} f g S = [,]-∘ S ∘ splitAt n
+
+ Push-unitaryʳ
+ : {n : ℕ}
+ (X : ∣ Values n ∣)
+ → Push.₁ (id Vec.++ (λ())) ⟨$⟩ (X ++ (<ε> {0})) ≋ X
+ Push-unitaryʳ {n} X i = begin
+ merge (X ++ <ε>) (preimage (id Vec.++ (λ ())) ⁅ i ⁆) ≡⟨ merge-cong₂ (X Vec.++ <ε>) (preimage-++′ id (λ ()) ⁅ i ⁆) ⟩
+ merge (X ++ <ε>) (⁅ i ⁆ Vec.++ preimage (λ ()) ⁅ i ⁆) ≡⟨ merge-++ X <ε> ⁅ i ⁆ (preimage (λ ()) ⁅ i ⁆) ⟩
+ join (merge X ⁅ i ⁆) (merge <ε> (preimage (λ ()) ⁅ i ⁆)) ≡⟨ ≡.cong (join (merge X ⁅ i ⁆)) (merge-[] <ε> (preimage (λ ()) ⁅ i ⁆)) ⟩
+ join (merge X ⁅ i ⁆) U ≡⟨ join-comm (merge X ⁅ i ⁆) U ⟩
+ merge X ⁅ i ⁆ ≡⟨ merge-⁅⁆ X i ⟩
+ X i ∎
+
+ Push-swap
+ : {n m : ℕ}
+ (X : ∣ Values n ∣)
+ (Y : ∣ Values m ∣)
+ → Push.₁ (+-swap {m}) ⟨$⟩ (X ++ Y) ≋ (Y ++ X)
+ Push-swap {n} {m} X Y i = begin
+ merge (X ++ Y) (preimage (+-swap {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ n+m↔m+n (X ++ Y) ⁅ i ⁆ ⟩
+ merge ((X ++ Y) ∘ +-swap {n}) ⁅ i ⁆ ≡⟨ merge-⁅⁆ ((X ++ Y) ∘ (+-swap {n})) i ⟩
+ ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
+ [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩
+ [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
+ [ Y , X ]′ (splitAt m i) ≡⟨⟩
+ (Y ++ X) i ∎
+ where
+ open ≡-Reasoning
+ open Inverse
+ module +-swap = _≅_ (+-comm {m} {n})
+ n+m↔m+n : Permutation (n + m) (m + n)
+ n+m↔m+n .to = +-swap.to
+ n+m↔m+n .from = +-swap.from
+ n+m↔m+n .to-cong ≡.refl = ≡.refl
+ n+m↔m+n .from-cong ≡.refl = ≡.refl
+ n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ })
+
+open SymmetricMonoidalFunctor
+Push,++,[] : SymmetricMonoidalFunctor
+Push,++,[] .F = Push
+Push,++,[] .isBraidedMonoidal = record
+ { isMonoidal = record
+ { ε = Push-ε
+ ; ⊗-homo = ⊗-homomorphism
+ ; associativity = λ { {n} {m} {o} {(X , Y) , Z} → Push-assoc X Y Z }
+ ; unitaryˡ = λ { {n} {_ , X} → Push-unitaryˡ X }
+ ; unitaryʳ = λ { {n} {X , _} → Push-unitaryʳ X }
+ }
+ ; braiding-compat = λ { {n} {m} {X , Y} → Push-swap X Y }
+ }
+
+module Push,++,[] = SymmetricMonoidalFunctor Push,++,[]
diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda
new file mode 100644
index 0000000..6659fb3
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/System.agda
@@ -0,0 +1,394 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Monoidal.Instance.Nat.System where
+
+import Categories.Category.Monoidal.Utilities as ⊗-Util
+import Data.Circuit.Value as Value
+import Data.Vec.Functional as Vec
+import Relation.Binary.PropositionalEquality as ≡
+
+open import Level using (0ℓ; suc; Level)
+
+open import Category.Monoidal.Instance.Nat using (Nat,+,0; Natop,+,0)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using () renaming (Setoids-× to 0ℓ-Setoids-×)
+open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
+
+module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B)
+module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B)
+
+open import Functor.Monoidal.Instance.Nat.Pull using (Pull,++,[])
+open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using (module Strong)
+
+Pull,++,[]B : Strong.BraidedMonoidalFunctor
+Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
+module Pull,++,[]B = Strong.BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
+
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian; Natop)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Categories.Category.Product using (Product)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Functor using (Functor)
+open import Categories.Functor using (_∘F_)
+open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
+open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Product using (_,_; dmap; _×_) renaming (map to ×-map)
+open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ; swapₛ)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (_⇒ₛ_; ∣_∣)
+open import Data.System {suc 0ℓ} using (Systemₛ; System; discrete; _≤_)
+open import Data.System.Values Monoid using (++ₛ; splitₛ; Values; ++-cong; _++_; [])
+open import Data.System.Values Value.Monoid using (_≋_; module ≋)
+open import Data.Unit.Polymorphic using (⊤; tt)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id; case_of_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_; setoid)
+open import Functor.Instance.Nat.Pull using (Pull)
+open import Functor.Instance.Nat.Push using (Push)
+open import Functor.Instance.Nat.System using (Sys; Sys-defs)
+open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv)
+open import Functor.Monoidal.Instance.Nat.Push using (Push,++,[])
+open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (associativity-inv)
+open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; unitaryˡ-inv; module Shorthands)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+
+open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_)
+
+open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
+
+open BinaryProducts products using (-×-)
+open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap; +₁∘i₁; +₁∘i₂)
+open Dual.op-binaryProducts using () renaming (×-assoc to +-assoc)
+open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B)
+
+open Func
+
+Sys-ε : ⊤ₛ {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0
+Sys-ε = Const ⊤ₛ (Systemₛ 0) (discrete 0)
+
+private
+
+ variable
+ n m o : ℕ
+ c₁ c₂ c₃ c₄ c₅ c₆ : Level
+ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level
+
+_×-⇒_
+ : {A : Setoid c₁ ℓ₁}
+ {B : Setoid c₂ ℓ₂}
+ {C : Setoid c₃ ℓ₃}
+ {D : Setoid c₄ ℓ₄}
+ {E : Setoid c₅ ℓ₅}
+ {F : Setoid c₆ ℓ₆}
+ → A ⟶ₛ B ⇒ₛ C
+ → D ⟶ₛ E ⇒ₛ F
+ → A ×ₛ D ⟶ₛ B ×ₛ E ⇒ₛ C ×ₛ F
+_×-⇒_ f g .to (x , y) = to f x ×-function to g y
+_×-⇒_ f g .cong (x , y) = cong f x , cong g y
+
+⊗ : System n × System m → System (n + m)
+⊗ {n} {m} (S₁ , S₂) = record
+ { S = S₁.S ×ₛ S₂.S
+ ; fₛ = S₁.fₛ ×-⇒ S₂.fₛ ∙ splitₛ
+ ; fₒ = ++ₛ ∙ S₁.fₒ ×-function S₂.fₒ
+ }
+ where
+ module S₁ = System S₁
+ module S₂ = System S₂
+
+opaque
+
+ _~_ : {A B : Setoid 0ℓ 0ℓ} → Func A B → Func A B → Set
+ _~_ = _≈_
+ infix 4 _~_
+
+ sym-~
+ : {A B : Setoid 0ℓ 0ℓ}
+ {x y : Func A B}
+ → x ~ y
+ → y ~ x
+ sym-~ {A} {B} {x} {y} = 0ℓ-Setoids-×.Equiv.sym {A} {B} {x} {y}
+
+⊗ₛ
+ : {n m : ℕ}
+ → Systemₛ n ×ₛ Systemₛ m ⟶ₛ Systemₛ (n + m)
+⊗ₛ .to = ⊗
+⊗ₛ {n} {m} .cong {a , b} {c , d} ((a≤c , c≤a) , (b≤d , d≤b)) = left , right
+ where
+ module a = System a
+ module b = System b
+ module c = System c
+ module d = System d
+ module a≤c = _≤_ a≤c
+ module b≤d = _≤_ b≤d
+ module c≤a = _≤_ c≤a
+ module d≤b = _≤_ d≤b
+
+ open _≤_
+ left : ⊗ₛ ⟨$⟩ (a , b) ≤ ⊗ₛ ⟨$⟩ (c , d)
+ left .⇒S = a≤c.⇒S ×-function b≤d.⇒S
+ left .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (a≤c.≗-fₛ i₁) (b≤d.≗-fₛ i₂)
+ left .≗-fₒ = cong ++ₛ ∘ dmap a≤c.≗-fₒ b≤d.≗-fₒ
+
+ right : ⊗ₛ ⟨$⟩ (c , d) ≤ ⊗ₛ ⟨$⟩ (a , b)
+ right .⇒S = c≤a.⇒S ×-function d≤b.⇒S
+ right .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (c≤a.≗-fₛ i₁) (d≤b.≗-fₛ i₂)
+ right .≗-fₒ = cong ++ₛ ∘ dmap c≤a.≗-fₒ d≤b.≗-fₒ
+
+opaque
+
+ unfolding Sys-defs
+
+ System-⊗-≤
+ : {n n′ m m′ : ℕ}
+ (X : System n)
+ (Y : System m)
+ (f : Fin n → Fin n′)
+ (g : Fin m → Fin m′)
+ → ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y) ≤ Sys.₁ (f +₁ g) ⟨$⟩ ⊗ (X , Y)
+ System-⊗-≤ {n} {n′} {m} {m′} X Y f g = record
+ { ⇒S = Id (X.S ×ₛ Y.S)
+ ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.sym-commute (f , g) {i}) {s}
+ ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂}
+ }
+ where
+ module X = System X
+ module Y = System Y
+
+ System-⊗-≥
+ : {n n′ m m′ : ℕ}
+ (X : System n)
+ (Y : System m)
+ (f : Fin n → Fin n′)
+ (g : Fin m → Fin m′)
+ → Sys.₁ (f +₁ g) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y)
+ System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record
+ { ⇒S = Id (X.S ×ₛ Y.S)
+ ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.commute (f , g) {i}) {s}
+ ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.sym-commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂}
+ }
+ where
+ module X = System X
+ module Y = System Y
+
+⊗-homomorphism : NaturalTransformation (-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -+-)
+⊗-homomorphism = ntHelper record
+ { η = λ (n , m) → ⊗ₛ {n} {m}
+ ; commute = λ { (f , g) {X , Y} → System-⊗-≤ X Y f g , System-⊗-≥ X Y f g }
+ }
+
+opaque
+
+ unfolding Sys-defs
+
+ ⊗-assoc-≤
+ : (X : System n)
+ (Y : System m)
+ (Z : System o)
+ → Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z)) ≤ ⊗ (X , ⊗ (Y , Z))
+ ⊗-assoc-≤ {n} {m} {o} X Y Z = record
+ { ⇒S = assocˡ
+ ; ≗-fₛ = λ i ((s₁ , s₂) , s₃) → cong (X.fₛ ×-⇒ (Y.fₛ ×-⇒ Z.fₛ) ∙ assocˡ) (associativity-inv {x = i}) {s₁ , s₂ , s₃}
+ ; ≗-fₒ = λ ((s₁ , s₂) , s₃) → Push,++,[].associativity {x = (X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
+ }
+ where
+ open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products)
+ open BinaryProducts 0ℓ-products using (assocˡ)
+
+ module X = System X
+ module Y = System Y
+ module Z = System Z
+
+ ⊗-assoc-≥
+ : (X : System n)
+ (Y : System m)
+ (Z : System o)
+ → ⊗ (X , ⊗ (Y , Z)) ≤ Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z))
+ ⊗-assoc-≥ {n} {m} {o} X Y Z = record
+ { ⇒S = ×-assocʳ
+ ; ≗-fₛ = λ i (s₁ , s₂ , s₃) → cong ((X.fₛ ×-⇒ Y.fₛ) ×-⇒ Z.fₛ) (sym-split-assoc {i}) {(s₁ , s₂) , s₃}
+ ; ≗-fₒ = λ (s₁ , s₂ , s₃) → sym-++-assoc {(X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
+ }
+ where
+ open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod)
+ open BinaryProducts prod using () renaming (assocʳ to ×-assocʳ; assocˡ to ×-assocˡ)
+
+ +-assocℓ : Fin ((n + m) + o) → Fin (n + (m + o))
+ +-assocℓ = +-assocˡ {n} {m} {o}
+
+ opaque
+
+ unfolding _~_
+
+ associativity-inv-~ : splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ ~ ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ
+ associativity-inv-~ {i} = associativity-inv {n} {m} {o} {i}
+
+ associativity-~ : Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) ~ ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ
+ associativity-~ {i} = Push,++,[].associativity {n} {m} {o} {i}
+
+ sym-split-assoc-~ : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ~ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ
+ sym-split-assoc-~ = sym-~ associativity-inv-~
+
+ sym-++-assoc-~ : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ~ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
+ sym-++-assoc-~ = sym-~ associativity-~
+
+ opaque
+
+ unfolding _~_
+
+ sym-split-assoc : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ≈ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ
+ sym-split-assoc {i} = sym-split-assoc-~ {i}
+
+ sym-++-assoc : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ≈ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
+ sym-++-assoc {i} = sym-++-assoc-~
+
+ module X = System X
+ module Y = System Y
+ module Z = System Z
+
+ Sys-unitaryˡ-≤ : (X : System n) → Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X)) ≤ X
+ Sys-unitaryˡ-≤ {n} X = record
+ { ⇒S = proj₂ₛ
+ ; ≗-fₛ = λ i (_ , s) → cong (X.fₛ ∙ proj₂ₛ {A = ⊤ₛ {0ℓ}}) (unitaryˡ-inv {n} {i})
+ ; ≗-fₒ = λ (_ , s) → Push,++,[].unitaryˡ {n} {tt , X.fₒ′ s}
+ }
+ where
+ module X = System X
+
+ Sys-unitaryˡ-≥ : (X : System n) → X ≤ Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X))
+ Sys-unitaryˡ-≥ {n} X = record
+ { ⇒S = < Const X.S ⊤ₛ tt , Id X.S >ₛ
+ ; ≗-fₛ = λ i s → cong (disc.fₛ ×-⇒ X.fₛ ∙ ε⇒ ×-function Id (Values n)) (sym-split-unitaryˡ {i})
+ ; ≗-fₒ = λ s → sym-++-unitaryˡ {_ , X.fₒ′ s}
+ }
+ where
+ module X = System X
+ open SymmetricMonoidalCategory 0ℓ-Setoids-× using (module Equiv)
+ open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (λ⇐)
+ open Shorthands using (ε⇐; ε⇒)
+ module disc = System (discrete 0)
+ sym-split-unitaryˡ
+ : λ⇐ ≈ ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id)
+ sym-split-unitaryˡ =
+ 0ℓ-Setoids-×.Equiv.sym
+ {Values n}
+ {⊤ₛ ×ₛ Values n}
+ {ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id)}
+ {λ⇐}
+ (unitaryˡ-inv {n})
+ sym-++-unitaryˡ : proj₂ₛ {A = ⊤ₛ {0ℓ} {0ℓ}} ≈ Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n)
+ sym-++-unitaryˡ =
+ 0ℓ-Setoids-×.Equiv.sym
+ {⊤ₛ ×ₛ Values n}
+ {Values n}
+ {Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n)}
+ {proj₂ₛ}
+ (Push,++,[].unitaryˡ {n})
+
+
+ Sys-unitaryʳ-≤ : (X : System n) → Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0)) ≤ X
+ Sys-unitaryʳ-≤ {n} X = record
+ { ⇒S = proj₁ₛ
+ ; ≗-fₛ = λ i (s , _) → cong (X.fₛ ∙ proj₁ₛ {B = ⊤ₛ {0ℓ}}) (unitaryʳ-inv {n} {i})
+ ; ≗-fₒ = λ (s , _) → Push,++,[].unitaryʳ {n} {X.fₒ′ s , tt}
+ }
+ where
+ module X = System X
+
+ Sys-unitaryʳ-≥ : (X : System n) → X ≤ Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0))
+ Sys-unitaryʳ-≥ {n} X = record
+ { ⇒S = < Id X.S , Const X.S ⊤ₛ tt >ₛ
+ ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ disc.fₛ ∙ Id (Values n) ×-function ε⇒) sym-split-unitaryʳ {s , tt}
+ ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt}
+ }
+ where
+ module X = System X
+ module disc = System (discrete 0)
+ open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (ρ⇐)
+ open Shorthands using (ε⇐; ε⇒)
+ sym-split-unitaryʳ
+ : ρ⇐ ≈ Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ()))
+ sym-split-unitaryʳ =
+ 0ℓ-Setoids-×.Equiv.sym
+ {Values n}
+ {Values n ×ₛ ⊤ₛ}
+ {Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ()))}
+ {ρ⇐}
+ (unitaryʳ-inv {n})
+ sym-++-unitaryʳ : proj₁ₛ {B = ⊤ₛ {0ℓ}} ≈ Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε
+ sym-++-unitaryʳ =
+ 0ℓ-Setoids-×.Equiv.sym
+ {Values n ×ₛ ⊤ₛ}
+ {Values n}
+ {Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε}
+ {proj₁ₛ}
+ (Push,++,[].unitaryʳ {n})
+
+ Sys-braiding-compat-≤
+ : (X : System n)
+ (Y : System m)
+ → Sys.₁ (+-swap {m} {n}) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Y , X)
+ Sys-braiding-compat-≤ {n} {m} X Y = record
+ { ⇒S = swapₛ
+ ; ≗-fₛ = λ i (s₁ , s₂) → cong (Y.fₛ ×-⇒ X.fₛ ∙ swapₛ) (braiding-compat-inv {m} {n} {i}) {s₂ , s₁}
+ ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].braiding-compat {n} {m} {X.fₒ′ s₁ , Y.fₒ′ s₂}
+ }
+ where
+ module X = System X
+ module Y = System Y
+
+ Sys-braiding-compat-≥
+ : (X : System n)
+ (Y : System m)
+ → ⊗ (Y , X) ≤ Sys.₁ (+-swap {m} {n}) ⟨$⟩ ⊗ (X , Y)
+ Sys-braiding-compat-≥ {n} {m} X Y = record
+ { ⇒S = swapₛ
+ ; ≗-fₛ = λ i (s₂ , s₁) → cong (X.fₛ ×-⇒ Y.fₛ) (sym-braiding-compat-inv {i})
+ ; ≗-fₒ = λ (s₂ , s₁) → sym-braiding-compat-++ {X.fₒ′ s₁ , Y.fₒ′ s₂}
+ }
+ where
+ module X = System X
+ module Y = System Y
+ sym-braiding-compat-inv : swapₛ ∙ splitₛ {m} ≈ splitₛ ∙ Pull.₁ (+-swap {m} {n})
+ sym-braiding-compat-inv {i} =
+ 0ℓ-Setoids-×.Equiv.sym
+ {Values (m + n)}
+ {Values n ×ₛ Values m}
+ {splitₛ ∙ Pull.₁ (+-swap {m} {n})}
+ {swapₛ ∙ splitₛ {m}}
+ (λ {j} → braiding-compat-inv {m} {n} {j}) {i}
+ sym-braiding-compat-++ : ++ₛ {m} ∙ swapₛ ≈ Push.₁ (+-swap {m} {n}) ∙ ++ₛ
+ sym-braiding-compat-++ {i} =
+ 0ℓ-Setoids-×.Equiv.sym
+ {Values n ×ₛ Values m}
+ {Values (m + n)}
+ {Push.₁ (+-swap {m} {n}) ∙ ++ₛ}
+ {++ₛ {m} ∙ swapₛ}
+ (Push,++,[].braiding-compat {n} {m})
+
+open Lax.SymmetricMonoidalFunctor
+
+Sys,⊗,ε : Lax.SymmetricMonoidalFunctor
+Sys,⊗,ε .F = Sys
+Sys,⊗,ε .isBraidedMonoidal = record
+ { isMonoidal = record
+ { ε = Sys-ε
+ ; ⊗-homo = ⊗-homomorphism
+ ; associativity = λ { {n} {m} {o} {(X , Y), Z} → ⊗-assoc-≤ X Y Z , ⊗-assoc-≥ X Y Z }
+ ; unitaryˡ = λ { {n} {_ , X} → Sys-unitaryˡ-≤ X , Sys-unitaryˡ-≥ X }
+ ; unitaryʳ = λ { {n} {X , _} → Sys-unitaryʳ-≤ X , Sys-unitaryʳ-≥ X }
+ }
+ ; braiding-compat = λ { {n} {m} {X , Y} → Sys-braiding-compat-≤ X Y , Sys-braiding-compat-≥ X Y }
+ }
+
+module Sys,⊗,ε = Lax.SymmetricMonoidalFunctor Sys,⊗,ε
diff --git a/Functor/Monoidal/Strong/Properties.agda b/Functor/Monoidal/Strong/Properties.agda
new file mode 100644
index 0000000..9eb7579
--- /dev/null
+++ b/Functor/Monoidal/Strong/Properties.agda
@@ -0,0 +1,104 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+open import Categories.Category.Monoidal using (MonoidalCategory)
+open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
+
+module Functor.Monoidal.Strong.Properties
+ {o o′ ℓ ℓ′ e e′ : Level}
+ {C : MonoidalCategory o ℓ e}
+ {D : MonoidalCategory o′ ℓ′ e′}
+ (F,φ,ε : StrongMonoidalFunctor C D) where
+
+import Categories.Category.Monoidal.Utilities as ⊗-Utilities
+import Categories.Category.Construction.Core as Core
+
+open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+
+private
+
+ module C where
+ open MonoidalCategory C public
+ open ⊗-Utilities.Shorthands monoidal public using (α⇐; λ⇐; ρ⇐)
+
+ module D where
+ open MonoidalCategory D public
+ open ⊗-Utilities.Shorthands monoidal using (α⇐; λ⇐; ρ⇐) public
+ open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) public
+ open ⊗-Utilities monoidal using (_⊗ᵢ_) public
+
+open D
+
+open StrongMonoidalFunctor F,φ,ε
+
+private
+
+ variable
+ X Y Z : C.Obj
+
+ α : {A B C : Obj} → (A ⊗₀ B) ⊗₀ C ≅ A ⊗₀ (B ⊗₀ C)
+ α = associator
+
+ Fα : F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ≅ F₀ (X C.⊗₀ (Y C.⊗₀ Z))
+ Fα = [ F ]-resp-≅ C.associator
+
+ λ- : {A : Obj} → unit ⊗₀ A ≅ A
+ λ- = unitorˡ
+
+ Fλ : F₀ (C.unit C.⊗₀ X) ≅ F₀ X
+ Fλ = [ F ]-resp-≅ C.unitorˡ
+
+ ρ : {A : Obj} → A ⊗₀ unit ≅ A
+ ρ = unitorʳ
+
+ Fρ : F₀ (X C.⊗₀ C.unit) ≅ F₀ X
+ Fρ = [ F ]-resp-≅ C.unitorʳ
+
+ φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y)
+ φ = ⊗-homo.FX≅GX
+
+module Shorthands where
+
+ φ⇒ : F₀ X ⊗₀ F₀ Y ⇒ F₀ (X C.⊗₀ Y)
+ φ⇒ = ⊗-homo.⇒.η _
+
+ φ⇐ : F₀ (X C.⊗₀ Y) ⇒ F₀ X ⊗₀ F₀ Y
+ φ⇐ = ⊗-homo.⇐.η _
+
+ ε⇒ : unit ⇒ F₀ C.unit
+ ε⇒ = ε.from
+
+ ε⇐ : F₀ C.unit ⇒ unit
+ ε⇐ = ε.to
+
+open Shorthands
+open HomReasoning
+
+associativityᵢ : Fα {X} {Y} {Z} ∘ᵢ φ ∘ᵢ φ ⊗ᵢ idᵢ ≈ᵢ φ ∘ᵢ idᵢ ⊗ᵢ φ ∘ᵢ α
+associativityᵢ = ⌞ associativity ⌟
+
+associativity-inv : φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.α⇐ {X} {Y} {Z}) ≈ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐
+associativity-inv = begin
+ φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.α⇐ ≈⟨ sym-assoc ⟩
+ (φ⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.α⇐ ≈⟨ to-≈ associativityᵢ ⟩
+ (α⇐ ∘ id ⊗₁ φ⇐) ∘ φ⇐ ≈⟨ assoc ⟩
+ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ ∎
+
+unitaryˡᵢ : Fλ {X} ∘ᵢ φ ∘ᵢ ε ⊗ᵢ idᵢ ≈ᵢ λ-
+unitaryˡᵢ = ⌞ unitaryˡ ⌟
+
+unitaryˡ-inv : ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.λ⇐ {X}) ≈ λ⇐
+unitaryˡ-inv = begin
+ ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.λ⇐ ≈⟨ sym-assoc ⟩
+ (ε⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.λ⇐ ≈⟨ to-≈ unitaryˡᵢ ⟩
+ λ⇐ ∎
+
+unitaryʳᵢ : Fρ {X} ∘ᵢ φ ∘ᵢ idᵢ ⊗ᵢ ε ≈ᵢ ρ
+unitaryʳᵢ = ⌞ unitaryʳ ⌟
+
+unitaryʳ-inv : id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ (C.ρ⇐ {X}) ≈ ρ⇐
+unitaryʳ-inv = begin
+ id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ C.ρ⇐ ≈⟨ sym-assoc ⟩
+ (id ⊗₁ ε⇐ ∘ φ⇐) ∘ F₁ C.ρ⇐ ≈⟨ to-≈ unitaryʳᵢ ⟩
+ ρ⇐ ∎
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-14 21:51:32 +0000