From 276418d0b0c1cd865c473a77db9c6e42ea9d02dc Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 5 Aug 2026 01:24:33 -0500 Subject: Finish merge and split symmetric monoidal functors --- Data/WiringDiagram/Looped/Monoidal.agda | 214 ----------------------- Data/WiringDiagram/Looped/Monoidal/Merge.agda | 242 ++++++++++++++++++++++++++ Data/WiringDiagram/Looped/Monoidal/Split.agda | 242 ++++++++++++++++++++++++++ 3 files changed, 484 insertions(+), 214 deletions(-) delete mode 100644 Data/WiringDiagram/Looped/Monoidal.agda create mode 100644 Data/WiringDiagram/Looped/Monoidal/Merge.agda create mode 100644 Data/WiringDiagram/Looped/Monoidal/Split.agda (limited to 'Data/WiringDiagram') diff --git a/Data/WiringDiagram/Looped/Monoidal.agda b/Data/WiringDiagram/Looped/Monoidal.agda deleted file mode 100644 index d0115ac..0000000 --- a/Data/WiringDiagram/Looped/Monoidal.agda +++ /dev/null @@ -1,214 +0,0 @@ -{-# OPTIONS --without-K --safe #-} -{-# OPTIONS --lossy-unification #-} - -open import Categories.Category using (Category) -open import Categories.Category.Monoidal.Bundle using (MonoidalCategory) -open import Categories.Functor using (Functor; _∘F_) -open import Categories.Functor.Monoidal using (StrongMonoidalFunctor; MonoidalFunctor; IsMonoidalFunctor) -open import Category.Dagger.2-Poset using (Map) -open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) -open import Category.KaroubiComplete using (KaroubiComplete) -open import Data.WiringDiagram.Monoidal using (BWD-MC) -open import Level using (Level; suc; _⊔_) - -open MonoidalCategory using (U) - -module Data.WiringDiagram.Looped.Monoidal - {o ℓ e o′ ℓ′ e′ : Level} - {𝒞 : Category o ℓ e} - {𝒟 : MonoidalCategory o′ ℓ′ e′} - {S : IdempotentSemiadditiveDagger 𝒞} - (let module S = IdempotentSemiadditiveDagger S) - (let S′ = S.semiadditiveDagger) - (karoubiComplete : KaroubiComplete (U 𝒟)) - (F : MonoidalFunctor (BWD-MC S′) 𝒟) - where - -module F = MonoidalFunctor F - -import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning -import Categories.Morphism.Reasoning as ⇒-Reasoning - -open import Categories.Category.Product using (_⁂_) -open import Categories.Functor.Properties using ([_]-resp-square) -open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Data.Product using (_,_) -open import Data.WiringDiagram.Balanced S′ using (Include; Push; Pull) -open import Data.WiringDiagram.Core S′ using (loop) -open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘push∘loop; loop∘pull∘loop) -open import Data.WiringDiagram.Looped.Core {S = S} karoubiComplete F.F using (Merge; Looped; π; forget; L; π∘l; forget∘π; π∘forget; l∘forget; l∘l) -open import Data.WiringDiagram.Monoidal S′ using (Push-MF; loop⊞loop; module BalancedPush) - -module BWD = BWD-MC S′ -module Merge = Functor Merge -module Push = Functor Push -module Push-MF = StrongMonoidalFunctor Push-MF -module maps-MC = MonoidalCategory S.maps-MC -module S-MC = MonoidalCategory S.monoidalCategory -module 𝒞 = Category 𝒞 -module 𝒟 = MonoidalCategory 𝒟 - -open BWD using () renaming (_∘_ to _∘′_; _⊗₁_ to _⊞₁_) -open BalancedPush using (Push-⊞₁; Push-assoc; Push-π₂; Push-π₁) -open Map using (map; entire) -open maps-MC using () renaming (_⊗₁_ to _⊗₁′_) -open 𝒟 using (_⇒_; _∘_; id; _≈_; _⊗₀_; _⊗₁_) -open S using (_⊕_; _×₁_) - -ε : 𝒟.unit ⇒ Looped maps-MC.unit -ε = π maps-MC.unit ∘ F.ε - -η : (X Y : 𝒞.Obj) → Looped X ⊗₀ Looped Y ⇒ Looped (X maps-MC.⊗₀ Y) -η X Y = π (X maps-MC.⊗₀ Y) ∘ F.⊗-homo.η (X , Y) ∘ forget X ⊗₁ forget Y - -private module Shorthands where - - φ : {X Y : 𝒞.Obj} → F.₀ X ⊗₀ F.₀ Y ⇒ F.₀ (X maps-MC.⊗₀ Y) - φ {X} {Y} = F.⊗-homo.η (X , Y) - - fo : {X : 𝒞.Obj} → Looped X ⇒ F.₀ X - fo {X} = forget X - - π′ : {X : 𝒞.Obj} → F.₀ X ⇒ Looped X - π′ {X} = π X - - L′ : {X : 𝒞.Obj} → F.₀ X ⇒ F.₀ X - L′ {X} = L X - -comm - : {X X′ Y Y′ : 𝒞.Obj} - (f : X maps-MC.⇒ X′) - (g : Y maps-MC.⇒ Y′) - → η X′ Y′ ∘ Merge.₁ f ⊗₁ Merge.₁ g 𝒟.≈ Merge.₁ (f maps-MC.⊗₁ g) ∘ η X Y -comm {X} {X′} {Y} {Y′} f g = begin - (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ (π′ ∘ F.₁ (Push.₁ f′) ∘ fo) ⊗₁ (π′ ∘ F.₁ (Push.₁ g′) ∘ fo) ≈⟨ pullʳ (pullʳ (sym ⊗-distrib-over-∘)) ⟩ - π′ ∘ φ ∘ (fo ∘ π X′ ∘ F.₁ (Push.₁ f′) ∘ fo) ⊗₁ (fo ∘ π Y′ ∘ F.₁ (Push.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π X′) ⟩⊗⟨ pullˡ (forget∘π Y′) ⟩ - π′ ∘ φ ∘ (L X′ ∘ F.₁ (Push.₁ f′) ∘ fo) ⊗₁ (L Y′ ∘ F.₁ (Push.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩⊗⟨ pushˡ F.homomorphism ⟨ - π′ ∘ φ ∘ (F.₁ (loop ∘′ Push.₁ f′) ∘ fo) ⊗₁ (F.₁ (loop ∘′ Push.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ - π′ ∘ φ ∘ F.₁ (loop ∘′ Push.₁ f′) ⊗₁ F.₁ (loop ∘′ Push.₁ g′) ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩   - π′ ∘ F.₁ ((loop ∘′ Push.₁ f′) ⊞₁ (loop ∘′ Push.₁ g′)) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (⊗-Reasoning.⊗-distrib-over-∘ BWD.monoidal) ⟩∘⟨refl ⟩ - π′ ∘ F.₁ (loop ⊞₁ loop ∘′ Push.₁ f′ ⊞₁ Push.₁ g′) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (BWD.∘-resp-≈ˡ loop⊞loop) ⟩∘⟨refl ⟩ - π′ ∘ F.₁ (loop ∘′ Push.₁ f′ ⊞₁ Push.₁ g′) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (BWD.∘-resp-≈ʳ (Push-⊞₁ f′ g′)) ⟩∘⟨refl ⟩ - π′ ∘ F.₁ (loop ∘′ Push.₁ (f′ ×₁ g′)) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (loop∘push∘loop (f′ ×₁ g′) (entire (f ⊗₁′ g))) ⟩∘⟨refl ⟨ - π′ ∘ F.₁ (loop ∘′ Push.₁ (f′ ×₁ g′) ∘′ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ - π′ ∘ L (X′ ⊕ Y′) ∘ F.₁ (Push.₁ (f′ ×₁ g′) ∘′ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ - π′ ∘ L (X′ ⊕ Y′) ∘ F.₁ (Push.₁ (f′ ×₁ g′)) ∘ L (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ≈⟨ pullˡ (π∘l (X′ ⊕ Y′)) ⟩ - π′ ∘ F.₁ (Push.₁ (f′ ×₁ g′)) ∘ L (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ≈⟨ pushʳ (pushʳ (pushˡ (sym (forget∘π (X ⊕ Y))))) ⟩ - (π′ ∘ F.₁ (Push.₁ (f′ ×₁ g′)) ∘ forget (X ⊕ Y)) ∘ π (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ∎ - where - f′ : X 𝒞.⇒ X′ - f′ = map f - g′ : Y 𝒞.⇒ Y′ - g′ = map g - open Shorthands - open 𝒟.Equiv - open ⊗-Reasoning 𝒟.monoidal - open ⇒-Reasoning (U 𝒟) - -⊗-homo : NaturalTransformation (𝒟.⊗ ∘F (Merge ⁂ Merge)) (Merge ∘F maps-MC.⊗) -⊗-homo = ntHelper record - { η = λ (X , Y) → η X Y - ; commute = λ (f , g) → comm f g - } - -associativity - : {X Y Z : 𝒞.Obj} - → Merge.₁ maps-MC.associator.from ∘ η (X ⊕ Y) Z ∘ η X Y ⊗₁ id ≈ η X (Y ⊕ Z) ∘ id ⊗₁ η Y Z ∘ 𝒟.associator.from -associativity {X} {Y} {Z} = begin - (π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ fo) ∘ η (X ⊕ Y) Z ∘ η X Y ⊗₁ id ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π ((X ⊕ Y) ⊕ Z))))) ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ η X Y ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (fo ∘ π′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π (X ⊕ Y)) ⟩⊗⟨refl ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (L′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (l∘forget Z) ⟨ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (L′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ (L′ ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ L′ ⊗₁ L′ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ _ ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ L′ ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (l∘l ((X ⊕ Y) ⊕ Z)) ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ ∘′ loop) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ pushˡ (sym (π∘l (X ⊕ (Y ⊕ Z)))) ⟩ - π′ ∘ L′ ∘ F.₁ (Push.₁ S.assocˡ ∘′ loop) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ - π′ ∘ F.₁ (loop ∘′ Push.₁ S.assocˡ ∘′ loop) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (loop∘push∘loop S.assocˡ (entire maps-MC.associator.from)) ⟩∘⟨refl ⟩ - π′ ∘ F.₁ (loop ∘′ Push.₁ S.assocˡ) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ - π′ ∘ L′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ pullˡ (π∘l (X ⊕ (Y ⊕ Z))) ⟩ - π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push-assoc ⟩∘⟨ pushʳ split₁ˡ ⟩ - π′ ∘ F.₁ BWD.associator.from ∘ (φ ∘ φ ⊗₁ id) ∘ (fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ F.associativity ⟩ - π′ ∘ φ ∘ (id ⊗₁ φ ∘ 𝒟.associator.from) ∘ (fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ 𝒟.assoc-commute-from ⟩ - π′ ∘ φ ∘ id ⊗₁ φ ∘ fo ⊗₁ (fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - π′ ∘ φ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ pushˡ (sym (π∘l (X ⊕ (Y ⊕ Z)))) ⟩ - π′ ∘ L′ ∘ φ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟨ - π′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.sym-commute _) ⟩ - π′ ∘ φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩ - π′ ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget X ⟩⊗⟨ pushˡ (sym (forget∘π (Y ⊕ Z))) ⟩∘⟨refl ⟩ - π′ ∘ φ ∘ fo ⊗₁ (fo ∘ π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ pushʳ (pushʳ (pushˡ split₂ʳ)) ⟩ - (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ∎ - where - open Shorthands - open ⊗-Reasoning 𝒟.monoidal - open ⇒-Reasoning 𝒟.U - open 𝒟.Equiv - -unitaryˡ - : {X : 𝒞.Obj} - → Merge.₁ maps-MC.unitorˡ.from ∘ η maps-MC.unit X ∘ ε ⊗₁ id ≈ 𝒟.unitorˡ.from -unitaryˡ {X} = begin - (π′ ∘ F.₁ (Push.₁ S.π₂) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π (S.𝟘 ⊕ X))))) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ (fo ∘ ε) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π S.𝟘) ⟩⊗⟨ sym (l∘forget X) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ (L′ ∘ F.ε) ⊗₁ (L′ ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ L′ ⊗₁ L′ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ L′ ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (l∘l (S.𝟘 ⊕ X)) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂ ∘′ loop) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ pushˡ (sym (π∘l X)) ⟩ - π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₂ ∘′ loop) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ ([ F.F ]-resp-square (loop∘push∘loop S.π₂ (entire maps-MC.unitorˡ.from))) ⟩ - π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₂) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ pullˡ (π∘l X) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₂) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push-π₂ ⟩∘⟨ pushʳ serialize₁₂ ⟩ - π′ ∘ F.₁ BWD.unitorˡ.from ∘ (φ ∘ F.ε ⊗₁ id) ∘ id ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ F.unitaryˡ ⟩ - π′ ∘ 𝒟.unitorˡ.from ∘ id ⊗₁ fo ≈⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-from ⟩ - π′ ∘ fo ∘ 𝒟.unitorˡ.from ≈⟨ cancelˡ (π∘forget X) ⟩ - 𝒟.unitorˡ.from ∎ - where - open Shorthands - open ⊗-Reasoning 𝒟.monoidal - open ⇒-Reasoning 𝒟.U - open 𝒟.Equiv - -unitaryʳ - : {X : 𝒞.Obj} - → Merge.₁ maps-MC.unitorʳ.from ∘ η X maps-MC.unit ∘ id ⊗₁ ε ≈ 𝒟.unitorʳ.from -unitaryʳ {X} = begin - (π′ ∘ F.₁ (Push.₁ S.π₁) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π (X ⊕ S.𝟘))))) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ merge₂ʳ ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ fo ⊗₁ (fo ∘ ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (l∘forget X) ⟩⊗⟨ pullˡ (forget∘π S.𝟘) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ F.ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ L′ ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (l∘l (X ⊕ S.𝟘)) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁ ∘′ loop) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ pushˡ (sym (π∘l X)) ⟩ - π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₁ ∘′ loop) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ extendʳ ([ F.F ]-resp-square (loop∘push∘loop S.π₁ (entire maps-MC.unitorʳ.from))) ⟩ - π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₁) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ pullˡ (π∘l X) ⟩ - π′ ∘ F.₁ (Push.₁ S.π₁) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push-π₁ ⟩∘⟨ pushʳ serialize₂₁ ⟩ - π′ ∘ F.₁ BWD.unitorʳ.from ∘ (φ ∘ id ⊗₁ F.ε) ∘ fo ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ F.unitaryʳ ⟩ - π′ ∘ 𝒟.unitorʳ.from ∘ fo ⊗₁ id ≈⟨ refl⟩∘⟨ 𝒟.unitorʳ-commute-from ⟩ - π′ ∘ fo ∘ 𝒟.unitorʳ.from ≈⟨ cancelˡ (π∘forget X) ⟩ - 𝒟.unitorʳ.from ∎ - where - open Shorthands - open ⊗-Reasoning 𝒟.monoidal - open ⇒-Reasoning 𝒟.U - open 𝒟.Equiv - -Merge-IsMF : IsMonoidalFunctor S.maps-MC 𝒟 Merge -Merge-IsMF = record - { ε = ε - ; ⊗-homo = ⊗-homo - ; associativity = associativity - ; unitaryˡ = unitaryˡ - ; unitaryʳ = unitaryʳ - } - -Merge-MF : MonoidalFunctor S.maps-MC 𝒟 -Merge-MF = record - { F = Merge - ; isMonoidal = Merge-IsMF - } diff --git a/Data/WiringDiagram/Looped/Monoidal/Merge.agda b/Data/WiringDiagram/Looped/Monoidal/Merge.agda new file mode 100644 index 0000000..5a0f05b --- /dev/null +++ b/Data/WiringDiagram/Looped/Monoidal/Merge.agda @@ -0,0 +1,242 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor using (Functor; _∘F_) +open import Categories.Functor.Monoidal using (StrongMonoidalFunctor; MonoidalFunctor; IsMonoidalFunctor) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Dagger.2-Poset using (Map) +open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.KaroubiComplete using (KaroubiComplete) +open import Data.WiringDiagram.Monoidal using (BWD-SMC) +open import Level using (Level; suc; _⊔_) + +open SymmetricMonoidalCategory using (U) + +module Data.WiringDiagram.Looped.Monoidal.Merge + {o ℓ e o′ ℓ′ e′ : Level} + {𝒞 : Category o ℓ e} + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + {S : IdempotentSemiadditiveDagger 𝒞} + (let module S = IdempotentSemiadditiveDagger S) + (let S′ = S.semiadditiveDagger) + (karoubiComplete : KaroubiComplete (U 𝒟)) + (F : Lax.SymmetricMonoidalFunctor (BWD-SMC S′) 𝒟) + where + +module F = Lax.SymmetricMonoidalFunctor F + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor.Properties using ([_]-resp-square) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Data.Product using (_,_) +open import Data.WiringDiagram.Balanced S′ using (Include; Push) +open import Data.WiringDiagram.Core S′ using (loop) +open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘push∘loop) +open import Data.WiringDiagram.Looped.Core {S = S} karoubiComplete F.F using (Merge; Looped; π; forget; L; π∘l; forget∘π; π∘forget; l∘forget; l∘l) +open import Data.WiringDiagram.Monoidal S′ using (Push-MF; loop⊞loop; module BalancedPush) + +module BWD = BWD-SMC S′ +module Merge = Functor Merge +module Push = Functor Push +module Push-MF = StrongMonoidalFunctor Push-MF +module maps-MC = MonoidalCategory S.maps-MC +module maps-SMC = SymmetricMonoidalCategory S.maps-SMC +module S-MC = MonoidalCategory S.monoidalCategory +module 𝒞 = Category 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 + +open BWD using () renaming (_∘_ to _∘′_; _⊗₁_ to _⊞₁_) +open BalancedPush using (Push-⊞₁; Push-assoc; Push-π₂; Push-π₁; Push-swap) +open Map using (map; entire) +open maps-MC using () renaming (_⊗₁_ to _⊗₁′_) +open 𝒟 using (_⇒_; _∘_; id; _≈_; _⊗₀_; _⊗₁_) +open S using (_⊕_; _×₁_) + +ε : 𝒟.unit ⇒ Looped maps-MC.unit +ε = π maps-MC.unit ∘ F.ε + +η : (X Y : 𝒞.Obj) → Looped X ⊗₀ Looped Y ⇒ Looped (X ⊕ Y) +η X Y = π (X ⊕ Y) ∘ F.⊗-homo.η (X , Y) ∘ forget X ⊗₁ forget Y + +private module Shorthands where + + φ : {X Y : 𝒞.Obj} → F.₀ X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊕ Y) + φ {X} {Y} = F.⊗-homo.η (X , Y) + + fo : {X : 𝒞.Obj} → Looped X ⇒ F.₀ X + fo {X} = forget X + + π′ : {X : 𝒞.Obj} → F.₀ X ⇒ Looped X + π′ {X} = π X + + L′ : {X : 𝒞.Obj} → F.₀ X ⇒ F.₀ X + L′ {X} = L X + +comm + : {X X′ Y Y′ : 𝒞.Obj} + (f : X maps-MC.⇒ X′) + (g : Y maps-MC.⇒ Y′) + → η X′ Y′ ∘ Merge.₁ f ⊗₁ Merge.₁ g ≈ Merge.₁ (f ⊗₁′ g) ∘ η X Y +comm {X} {X′} {Y} {Y′} f g = begin + (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ (π′ ∘ F.₁ (Push.₁ f′) ∘ fo) ⊗₁ (π′ ∘ F.₁ (Push.₁ g′) ∘ fo) ≈⟨ pullʳ (pullʳ (sym ⊗-distrib-over-∘)) ⟩ + π′ ∘ φ ∘ (fo ∘ π X′ ∘ F.₁ (Push.₁ f′) ∘ fo) ⊗₁ (fo ∘ π Y′ ∘ F.₁ (Push.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π X′) ⟩⊗⟨ pullˡ (forget∘π Y′) ⟩ + π′ ∘ φ ∘ (L X′ ∘ F.₁ (Push.₁ f′) ∘ fo) ⊗₁ (L Y′ ∘ F.₁ (Push.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩⊗⟨ pushˡ F.homomorphism ⟨ + π′ ∘ φ ∘ (F.₁ (loop ∘′ Push.₁ f′) ∘ fo) ⊗₁ (F.₁ (loop ∘′ Push.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ + π′ ∘ φ ∘ F.₁ (loop ∘′ Push.₁ f′) ⊗₁ F.₁ (loop ∘′ Push.₁ g′) ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩   + π′ ∘ F.₁ ((loop ∘′ Push.₁ f′) ⊞₁ (loop ∘′ Push.₁ g′)) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (⊗-Reasoning.⊗-distrib-over-∘ BWD.monoidal) ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (loop ⊞₁ loop ∘′ Push.₁ f′ ⊞₁ Push.₁ g′) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (BWD.∘-resp-≈ˡ loop⊞loop) ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (loop ∘′ Push.₁ f′ ⊞₁ Push.₁ g′) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (BWD.∘-resp-≈ʳ (Push-⊞₁ f′ g′)) ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (loop ∘′ Push.₁ (f′ ×₁ g′)) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (loop∘push∘loop (f′ ×₁ g′) (entire (f ⊗₁′ g))) ⟩∘⟨refl ⟨ + π′ ∘ F.₁ (loop ∘′ Push.₁ (f′ ×₁ g′) ∘′ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π′ ∘ L (X′ ⊕ Y′) ∘ F.₁ (Push.₁ (f′ ×₁ g′) ∘′ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π′ ∘ L (X′ ⊕ Y′) ∘ F.₁ (Push.₁ (f′ ×₁ g′)) ∘ L (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ≈⟨ pullˡ (π∘l (X′ ⊕ Y′)) ⟩ + π′ ∘ F.₁ (Push.₁ (f′ ×₁ g′)) ∘ L (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ≈⟨ pushʳ (pushʳ (pushˡ (sym (forget∘π (X ⊕ Y))))) ⟩ + (π′ ∘ F.₁ (Push.₁ (f′ ×₁ g′)) ∘ forget (X ⊕ Y)) ∘ π (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ∎ + where + f′ : X 𝒞.⇒ X′ + f′ = map f + g′ : Y 𝒞.⇒ Y′ + g′ = map g + open Shorthands + open 𝒟.Equiv + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning (U 𝒟) + +⊗-homo : NaturalTransformation (𝒟.⊗ ∘F (Merge ⁂ Merge)) (Merge ∘F maps-MC.⊗) +⊗-homo = ntHelper record + { η = λ (X , Y) → η X Y + ; commute = λ (f , g) → comm f g + } + +associativity + : {X Y Z : 𝒞.Obj} + → Merge.₁ maps-MC.associator.from ∘ η (X ⊕ Y) Z ∘ η X Y ⊗₁ id ≈ η X (Y ⊕ Z) ∘ id ⊗₁ η Y Z ∘ 𝒟.associator.from +associativity {X} {Y} {Z} = begin + (π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ fo) ∘ η (X ⊕ Y) Z ∘ η X Y ⊗₁ id ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π ((X ⊕ Y) ⊕ Z))))) ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ η X Y ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (fo ∘ π′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π (X ⊕ Y)) ⟩⊗⟨refl ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (L′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (l∘forget Z) ⟨ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (L′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ (L′ ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ L′ ⊗₁ L′ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ _ ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ L′ ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (l∘l ((X ⊕ Y) ⊕ Z)) ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ L′ ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ ∘′ loop) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ pushˡ (sym (π∘l (X ⊕ (Y ⊕ Z)))) ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.assocˡ ∘′ loop) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ + π′ ∘ F.₁ (loop ∘′ Push.₁ S.assocˡ ∘′ loop) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (loop∘push∘loop S.assocˡ (entire maps-MC.associator.from)) ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (loop ∘′ Push.₁ S.assocˡ) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ pullˡ (π∘l (X ⊕ (Y ⊕ Z))) ⟩ + π′ ∘ F.₁ (Push.₁ S.assocˡ) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push-assoc ⟩∘⟨ pushʳ split₁ˡ ⟩ + π′ ∘ F.₁ BWD.associator.from ∘ (φ ∘ φ ⊗₁ id) ∘ (fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ F.associativity ⟩ + π′ ∘ φ ∘ (id ⊗₁ φ ∘ 𝒟.associator.from) ∘ (fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ 𝒟.assoc-commute-from ⟩ + π′ ∘ φ ∘ id ⊗₁ φ ∘ fo ⊗₁ (fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ + π′ ∘ φ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ pushˡ (sym (π∘l (X ⊕ (Y ⊕ Z)))) ⟩ + π′ ∘ L′ ∘ φ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟨ + π′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.sym-commute _) ⟩ + π′ ∘ φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩ + π′ ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget X ⟩⊗⟨ pushˡ (sym (forget∘π (Y ⊕ Z))) ⟩∘⟨refl ⟩ + π′ ∘ φ ∘ fo ⊗₁ (fo ∘ π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ pushʳ (pushʳ (pushˡ split₂ʳ)) ⟩ + (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +unitaryˡ + : {X : 𝒞.Obj} + → Merge.₁ maps-MC.unitorˡ.from ∘ η maps-MC.unit X ∘ ε ⊗₁ id ≈ 𝒟.unitorˡ.from +unitaryˡ {X} = begin + (π′ ∘ F.₁ (Push.₁ S.π₂) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π (S.𝟘 ⊕ X))))) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ (fo ∘ ε) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π S.𝟘) ⟩⊗⟨ sym (l∘forget X) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ (L′ ∘ F.ε) ⊗₁ (L′ ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ L′ ⊗₁ L′ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ L′ ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (l∘l (S.𝟘 ⊕ X)) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ L′ ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂ ∘′ loop) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ pushˡ (sym (π∘l X)) ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₂ ∘′ loop) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ ([ F.F ]-resp-square (loop∘push∘loop S.π₂ (entire maps-MC.unitorˡ.from))) ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₂) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ pullˡ (π∘l X) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₂) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push-π₂ ⟩∘⟨ pushʳ serialize₁₂ ⟩ + π′ ∘ F.₁ BWD.unitorˡ.from ∘ (φ ∘ F.ε ⊗₁ id) ∘ id ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ F.unitaryˡ ⟩ + π′ ∘ 𝒟.unitorˡ.from ∘ id ⊗₁ fo ≈⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-from ⟩ + π′ ∘ fo ∘ 𝒟.unitorˡ.from ≈⟨ cancelˡ (π∘forget X) ⟩ + 𝒟.unitorˡ.from ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +unitaryʳ + : {X : 𝒞.Obj} + → Merge.₁ maps-MC.unitorʳ.from ∘ η X maps-MC.unit ∘ id ⊗₁ ε ≈ 𝒟.unitorʳ.from +unitaryʳ {X} = begin + (π′ ∘ F.₁ (Push.₁ S.π₁) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π (X ⊕ S.𝟘))))) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ merge₂ʳ ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ fo ⊗₁ (fo ∘ ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (l∘forget X) ⟩⊗⟨ pullˡ (forget∘π S.𝟘) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ F.ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ L′ ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (l∘l (X ⊕ S.𝟘)) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ L′ ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁ ∘′ loop) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ pushˡ (sym (π∘l X)) ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₁ ∘′ loop) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ extendʳ ([ F.F ]-resp-square (loop∘push∘loop S.π₁ (entire maps-MC.unitorʳ.from))) ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.π₁) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ pullˡ (π∘l X) ⟩ + π′ ∘ F.₁ (Push.₁ S.π₁) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push-π₁ ⟩∘⟨ pushʳ serialize₂₁ ⟩ + π′ ∘ F.₁ BWD.unitorʳ.from ∘ (φ ∘ id ⊗₁ F.ε) ∘ fo ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ F.unitaryʳ ⟩ + π′ ∘ 𝒟.unitorʳ.from ∘ fo ⊗₁ id ≈⟨ refl⟩∘⟨ 𝒟.unitorʳ-commute-from ⟩ + π′ ∘ fo ∘ 𝒟.unitorʳ.from ≈⟨ cancelˡ (π∘forget X) ⟩ + 𝒟.unitorʳ.from ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +Merge-IsMF : IsMonoidalFunctor S.maps-MC 𝒟.monoidalCategory Merge +Merge-IsMF = record + { ε = ε + ; ⊗-homo = ⊗-homo + ; associativity = associativity + ; unitaryˡ = unitaryˡ + ; unitaryʳ = unitaryʳ + } + +Merge-MF : MonoidalFunctor S.maps-MC 𝒟.monoidalCategory +Merge-MF = record + { F = Merge + ; isMonoidal = Merge-IsMF + } + +braiding-compat : {X Y : 𝒞.Obj} → Merge.₁ (maps-SMC.braiding.⇒.η (X , Y)) ∘ η X Y ≈ η Y X ∘ 𝒟.braiding.⇒.η (Merge.₀ X , Merge.₀ Y) +braiding-compat {X} {Y} = begin + (π′ ∘ F.₁ (Push.₁ S.swap) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ≈⟨ pullʳ (pullʳ (pullˡ (forget∘π (X ⊕ Y)))) ⟩ + π′ ∘ F.₁ (Push.₁ S.swap) ∘ L′ ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ (sym F.homomorphism) ⟩ + π′ ∘ F.₁ (Push.₁ S.swap ∘′ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ pushˡ (sym (π∘l (Y ⊕ X))) ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.swap ∘′ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ ([ F.F ]-resp-square (loop∘push∘loop S.swap (entire (maps-SMC.braiding.⇒.η _)))) ⟩ + π′ ∘ L′ ∘ F.₁ (Push.₁ S.swap) ∘ φ ∘ fo ⊗₁ fo ≈⟨ pullˡ (π∘l (Y ⊕ X)) ⟩ + π′ ∘ F.₁ (Push.₁ S.swap) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push-swap ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (BWD.braiding.⇒.η _) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ F.braiding-compat ⟩ + π′ ∘ φ ∘ 𝒟.braiding.⇒.η _ ∘ fo ⊗₁ fo ≈⟨ pushʳ (pushʳ (𝒟.braiding.⇒.commute _)) ⟩ + (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.braiding.⇒.η _ ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +Merge-SMF : Lax.SymmetricMonoidalFunctor S.maps-SMC 𝒟 +Merge-SMF = record + { F = Merge + ; isBraidedMonoidal = record + { isMonoidal = Merge-IsMF + ; braiding-compat = braiding-compat + } + } diff --git a/Data/WiringDiagram/Looped/Monoidal/Split.agda b/Data/WiringDiagram/Looped/Monoidal/Split.agda new file mode 100644 index 0000000..39150b9 --- /dev/null +++ b/Data/WiringDiagram/Looped/Monoidal/Split.agda @@ -0,0 +1,242 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor using (Functor; _∘F_) +open import Categories.Functor.Monoidal using (StrongMonoidalFunctor; MonoidalFunctor; IsMonoidalFunctor) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Dagger.2-Poset using (Map) +open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.KaroubiComplete using (KaroubiComplete) +open import Data.WiringDiagram.Monoidal using (BWD-SMC) +open import Level using (Level; suc; _⊔_) + +open SymmetricMonoidalCategory using (U) + +module Data.WiringDiagram.Looped.Monoidal.Split + {o ℓ e o′ ℓ′ e′ : Level} + {𝒞 : Category o ℓ e} + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + {S : IdempotentSemiadditiveDagger 𝒞} + (let module S = IdempotentSemiadditiveDagger S) + (let S′ = S.semiadditiveDagger) + (karoubiComplete : KaroubiComplete (U 𝒟)) + (F : Lax.SymmetricMonoidalFunctor (BWD-SMC S′) 𝒟) + where + +module F = Lax.SymmetricMonoidalFunctor F + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Data.Product using (_,_) +open import Data.WiringDiagram.Balanced S′ using (Include; Pull) +open import Data.WiringDiagram.Core S′ using (loop; id-⧈) +open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘pull∘loop; loop-𝟘) +open import Data.WiringDiagram.Looped.Core {S = S} karoubiComplete F.F using (Split; Looped; π; forget; L; π∘l; forget∘π; π∘forget; l∘forget; l∘l) +open import Data.WiringDiagram.Monoidal S′ using (Pull-MF; loop⊞loop; module BalancedPull) + +module BWD = BWD-SMC S′ +module Split = Functor Split +module Pull = Functor Pull +module Pull-MF = StrongMonoidalFunctor Pull-MF +module maps-MC = MonoidalCategory S.maps-MC +module maps-MC-op = MonoidalCategory maps-MC.op +module maps-SMC = SymmetricMonoidalCategory S.maps-SMC +module maps-SMC-op = SymmetricMonoidalCategory maps-SMC.op +module S-MC = MonoidalCategory S.monoidalCategory +module 𝒞 = Category 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 + +open BWD using () renaming (_∘_ to _∘′_; _⊗₁_ to _⊞₁_) +open BalancedPull using (Pull-⊞₁; Pull-assoc; Pull-i₂; Pull-i₁; Pull-swap) +open Map using (map; functional) +open maps-MC-op using () renaming (_⊗₁_ to _⊗₁′_) +open 𝒟 using (_⇒_; _∘_; id; _≈_; _⊗₀_; _⊗₁_) +open S using (_⊕_; _×₁_) + +ε : 𝒟.unit ⇒ Looped maps-MC.unit +ε = π maps-MC.unit ∘ F.ε + +η : (X Y : 𝒞.Obj) → Looped X ⊗₀ Looped Y ⇒ Looped (X ⊕ Y) +η X Y = π (X ⊕ Y) ∘ F.⊗-homo.η (X , Y) ∘ forget X ⊗₁ forget Y + +private module Shorthands where + + φ : {X Y : 𝒞.Obj} → F.₀ X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊕ Y) + φ {X} {Y} = F.⊗-homo.η (X , Y) + + fo : {X : 𝒞.Obj} → Looped X ⇒ F.₀ X + fo {X} = forget X + + π′ : {X : 𝒞.Obj} → F.₀ X ⇒ Looped X + π′ {X} = π X + + L′ : {X : 𝒞.Obj} → F.₀ X ⇒ F.₀ X + L′ {X} = L X + +comm + : {X X′ Y Y′ : 𝒞.Obj} + (f : X′ maps-MC.⇒ X) + (g : Y′ maps-MC.⇒ Y) + → η X′ Y′ ∘ Split.₁ f ⊗₁ Split.₁ g ≈ Split.₁ (f ⊗₁′ g) ∘ η X Y +comm {X} {X′} {Y} {Y′} f g = begin + (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ (π′ ∘ F.₁ (Pull.₁ f′) ∘ fo) ⊗₁ (π′ ∘ F.₁ (Pull.₁ g′) ∘ fo) ≈⟨ pullʳ (pullʳ (sym ⊗-distrib-over-∘)) ⟩ + π′ ∘ φ ∘ (fo ∘ π′ ∘ F.₁ (Pull.₁ f′) ∘ fo) ⊗₁ (fo ∘ π′ ∘ F.₁ (Pull.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π X′) ⟩⊗⟨ pullˡ (forget∘π Y′) ⟩ + π′ ∘ φ ∘ (L′ ∘ F.₁ (Pull.₁ f′) ∘ fo) ⊗₁ (L′ ∘ F.₁ (Pull.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ refl⟩∘⟨ l∘forget X) ⟩⊗⟨ (refl⟩∘⟨ refl⟩∘⟨ l∘forget Y) ⟨ + π′ ∘ φ ∘ (L′ ∘ F.₁ _ ∘ L′ ∘ fo) ⊗₁ (L′ ∘ F.₁ (Pull.₁ g′) ∘ L′ ∘ fo) + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ pullˡ (sym F.homomorphism)) ⟩⊗⟨ (refl⟩∘⟨ pullˡ (sym F.homomorphism)) ⟩ + π′ ∘ φ ∘ (L′ ∘ F.₁ (_ ∘′ loop) ∘ fo) ⊗₁ (L′ ∘ F.₁ (Pull.₁ g′ ∘′ loop) ∘ fo) + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ([ F.F ]-resp-∘ (loop∘pull∘loop f′ (functional f))) ⟩⊗⟨ pullˡ ([ F.F ]-resp-∘ (loop∘pull∘loop g′ (functional g))) ⟩ + π′ ∘ φ ∘ (F.₁ (Pull.₁ f′ ∘′ loop) ∘ fo) ⊗₁ (F.₁ (Pull.₁ g′ ∘′ loop) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩⊗⟨ pushˡ F.homomorphism ⟩ + π′ ∘ φ ∘ (F.₁ (Pull.₁ f′) ∘ L′ ∘ fo) ⊗₁ (F.₁ (Pull.₁ g′) ∘ L′ ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ (l∘forget X)) ⟩⊗⟨ (refl⟩∘⟨ (l∘forget Y)) ⟩ + π′ ∘ φ ∘ (F.₁ (Pull.₁ f′) ∘ fo) ⊗₁ (F.₁ (Pull.₁ g′) ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ + π′ ∘ φ ∘ F.₁ (Pull.₁ f′) ⊗₁ F.₁ (Pull.₁ g′) ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ + π′ ∘ F.₁ (Pull.₁ f′ ⊞₁ Pull.₁ g′) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ (Pull-⊞₁ f′ g′) ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ (f′ ×₁ g′)) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget X ⟩⊗⟨ l∘forget Y ⟨ + π′ ∘ F.₁ (Pull.₁ (f′ ×₁ g′)) ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ + π′ ∘ F.₁ (Pull.₁ (f′ ×₁ g′)) ∘ φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute _) ⟩ + π′ ∘ F.₁ (Pull.₁ (f′ ×₁ g′)) ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ (f′ ×₁ g′)) ∘ L (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ≈⟨ pushʳ (pushʳ (pushˡ (sym (forget∘π (X ⊕ Y))))) ⟩ + (π′ ∘ F.₁ (Pull.₁ (f′ ×₁ g′)) ∘ forget (X ⊕ Y)) ∘ π (X ⊕ Y) ∘ φ ∘ fo ⊗₁ fo ∎ + where + f′ : X′ 𝒞.⇒ X + f′ = map f + g′ : Y′ 𝒞.⇒ Y + g′ = map g + open Shorthands + open 𝒟.Equiv + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning (U 𝒟) + +⊗-homo : NaturalTransformation (𝒟.⊗ ∘F (Split ⁂ Split)) (Split ∘F maps-MC-op.⊗) +⊗-homo = ntHelper record + { η = λ (X , Y) → η X Y + ; commute = λ (f , g) → comm f g + } + +associativity + : {X Y Z : 𝒞.Obj} + → Split.₁ maps-MC-op.associator.from ∘ η (X ⊕ Y) Z ∘ η X Y ⊗₁ id ≈ η X (Y ⊕ Z) ∘ id ⊗₁ η Y Z ∘ 𝒟.associator.from +associativity {X} {Y} {Z} = begin + (π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ fo) ∘ η (X ⊕ Y) Z ∘ η X Y ⊗₁ id ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π ((X ⊕ Y) ⊕ Z))))) ⟩ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ η X Y ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟨ + π′ ∘ F.₁ (Pull.₁ _) ∘ F.₁ (loop ⊞₁ loop) ∘ (φ ∘ fo ⊗₁ fo) ∘ η X Y ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (extendʳ (F.⊗-homo.sym-commute _)) ⟩ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (L′ ⊗₁ L′ ∘ fo ⊗₁ fo) ∘ η X Y ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩∘⟨refl ⟨ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ fo) ∘ η X Y ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget (X ⊕ Y) ⟩⊗⟨ l∘forget Z ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ fo ⊗₁ fo ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (fo ∘ π′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π (X ⊕ Y)) ⟩⊗⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (L′ ∘ φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (F.F-resp-≈ loop⊞loop ⟩∘⟨refl) ⟩⊗⟨refl ⟨ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.sym-commute _) ⟩⊗⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩⊗⟨refl ⟨ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ fo)) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ l∘forget X ⟩⊗⟨ l∘forget Y) ⟩⊗⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.assocʳ) ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Pull-assoc ⟩∘⟨refl ⟩ + π′ ∘ F.₁ BWD.associator.from ∘ φ ∘ (φ ∘ fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushʳ split₁ˡ ⟩ + π′ ∘ F.₁ BWD.associator.from ∘ (φ ∘ φ ⊗₁ id) ∘ (fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ F.associativity ⟩ + π′ ∘ φ ∘ (id ⊗₁ φ ∘ 𝒟.associator.from) ∘ (fo ⊗₁ fo) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ 𝒟.assoc-commute-from ⟩ + π′ ∘ φ ∘ id ⊗₁ φ ∘ fo ⊗₁ (fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ + π′ ∘ φ ∘ fo ⊗₁ (φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ l∘forget Y ⟩⊗⟨ l∘forget Z) ⟩∘⟨refl ⟨ + π′ ∘ φ ∘ fo ⊗₁ (φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ fo)) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩∘⟨refl ⟩ + π′ ∘ φ ∘ fo ⊗₁ (φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ (F.⊗-homo.commute _) ⟩∘⟨refl ⟩ + π′ ∘ φ ∘ fo ⊗₁ (F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (F.F-resp-≈ loop⊞loop ⟩∘⟨refl) ⟩∘⟨refl ⟩ + π′ ∘ φ ∘ fo ⊗₁ (L′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ pushˡ (sym (forget∘π (Y ⊕ Z))) ⟩∘⟨refl ⟩ + π′ ∘ φ ∘ fo ⊗₁ (fo ∘ π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ≈⟨ pushʳ (pushʳ (pushˡ split₂ʳ)) ⟩ + (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.associator.from ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +unitaryˡ + : {X : 𝒞.Obj} + → Split.₁ maps-MC-op.unitorˡ.from ∘ η maps-MC-op.unit X ∘ ε ⊗₁ id ≈ 𝒟.unitorˡ.from +unitaryˡ {X} = begin + (π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π (S.𝟘 ⊕ X))))) ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟨ + π′ ∘ F.₁ _ ∘ F.₁ (loop ⊞₁ loop) ∘ (φ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (extendʳ (F.⊗-homo.sym-commute _)) ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ φ ∘ (L′ ⊗₁ L′ ∘ fo ⊗₁ fo) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩∘⟨refl ⟨ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ fo) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget S.𝟘 ⟩⊗⟨ l∘forget X ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ φ ∘ fo ⊗₁ fo ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ φ ∘ (fo ∘ ε) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (forget∘π S.𝟘) ⟩⊗⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ φ ∘ (F.₁ loop ∘ F.ε) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (F.F-resp-≈ loop-𝟘 ⟩∘⟨refl) ⟩⊗⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ φ ∘ (F.₁ id-⧈ ∘ F.ε) ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ F.identity ⟩⊗⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₂) ∘ φ ∘ F.ε ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Pull-i₂ ⟩∘⟨ pushʳ serialize₁₂ ⟩ + π′ ∘ F.₁ BWD.unitorˡ.from ∘ (φ ∘ F.ε ⊗₁ id) ∘ id ⊗₁ fo ≈⟨ refl⟩∘⟨ pullˡ F.unitaryˡ ⟩ + π′ ∘ 𝒟.unitorˡ.from ∘ id ⊗₁ fo ≈⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-from ⟩ + π′ ∘ fo ∘ 𝒟.unitorˡ.from ≈⟨ cancelˡ (π∘forget X) ⟩ + 𝒟.unitorˡ.from ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +unitaryʳ + : {X : 𝒞.Obj} + → Split.₁ maps-MC-op.unitorʳ.from ∘ η X maps-MC-op.unit ∘ id ⊗₁ ε ≈ 𝒟.unitorʳ.from +unitaryʳ {X} = begin + (π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ pullʳ (pullʳ (extendʳ (pullˡ (forget∘π (X ⊕ S.𝟘))))) ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ L′ ∘ (φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟨ + π′ ∘ F.₁ _ ∘ F.₁ (loop ⊞₁ loop) ∘ (φ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (extendʳ (F.⊗-homo.sym-commute _)) ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ φ ∘ (L′ ⊗₁ L′ ∘ fo ⊗₁ fo) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩∘⟨refl ⟨ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ fo) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget X ⟩⊗⟨ l∘forget S.𝟘 ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ φ ∘ fo ⊗₁ fo ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₂ʳ ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ φ ∘ fo ⊗₁ (fo ∘ ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ pullˡ (forget∘π S.𝟘) ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ φ ∘ fo ⊗₁ (F.₁ loop ∘ F.ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (F.F-resp-≈ loop-𝟘 ⟩∘⟨refl) ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ φ ∘ fo ⊗₁ (F.₁ id-⧈ ∘ F.ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ elimˡ F.identity ⟩ + π′ ∘ F.₁ (Pull.₁ S.i₁) ∘ φ ∘ fo ⊗₁ F.ε ≈⟨ refl⟩∘⟨ F.F-resp-≈ Pull-i₁ ⟩∘⟨ pushʳ serialize₂₁ ⟩ + π′ ∘ F.₁ BWD.unitorʳ.from ∘ (φ ∘ id ⊗₁ F.ε) ∘ fo ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ F.unitaryʳ ⟩ + π′ ∘ 𝒟.unitorʳ.from ∘ fo ⊗₁ id ≈⟨ refl⟩∘⟨ 𝒟.unitorʳ-commute-from ⟩ + π′ ∘ fo ∘ 𝒟.unitorʳ.from ≈⟨ cancelˡ (π∘forget X) ⟩ + 𝒟.unitorʳ.from ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +Split-IsMF : IsMonoidalFunctor maps-MC.op 𝒟.monoidalCategory Split +Split-IsMF = record + { ε = ε + ; ⊗-homo = ⊗-homo + ; associativity = associativity + ; unitaryˡ = unitaryˡ + ; unitaryʳ = unitaryʳ + } + +Split-MF : MonoidalFunctor maps-MC.op 𝒟.monoidalCategory +Split-MF = record + { F = Split + ; isMonoidal = Split-IsMF + } + +braiding-compat : {X Y : 𝒞.Obj} → Split.₁ (maps-SMC-op.braiding.⇒.η (X , Y)) ∘ η X Y ≈ η Y X ∘ 𝒟.braiding.⇒.η (Split.₀ X , Split.₀ Y) +braiding-compat {X} {Y} = begin + (π′ ∘ F.₁ (Pull.₁ S.swap) ∘ fo) ∘ (π′ ∘ φ ∘ fo ⊗₁ fo) ≈⟨ pullʳ (pullʳ (pullˡ (forget∘π (X ⊕ Y)))) ⟩ + π′ ∘ F.₁ (Pull.₁ S.swap) ∘ L′ ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ loop⊞loop ⟩∘⟨refl ⟨ + π′ ∘ F.₁ _ ∘ F.₁ (loop ⊞₁ loop) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.sym-commute _) ⟩ + π′ ∘ F.₁ (Pull.₁ S.swap) ∘ φ ∘ L′ ⊗₁ L′ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + π′ ∘ F.₁ (Pull.₁ S.swap) ∘ φ ∘ (L′ ∘ fo) ⊗₁ (L′ ∘ fo) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget X ⟩⊗⟨ l∘forget Y ⟩ + π′ ∘ F.₁ (Pull.₁ S.swap) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ F.F-resp-≈ Pull-swap ⟩∘⟨refl ⟩ + π′ ∘ F.₁ (BWD.braiding.⇒.η _) ∘ φ ∘ fo ⊗₁ fo ≈⟨ refl⟩∘⟨ extendʳ F.braiding-compat ⟩ + π′ ∘ φ ∘ 𝒟.braiding.⇒.η _ ∘ fo ⊗₁ fo ≈⟨ pushʳ (pushʳ (𝒟.braiding.⇒.commute _)) ⟩ + (π′ ∘ φ ∘ fo ⊗₁ fo) ∘ 𝒟.braiding.⇒.η _ ∎ + where + open Shorthands + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + +Split-SMF : Lax.SymmetricMonoidalFunctor maps-SMC.op 𝒟 +Split-SMF = record + { F = Split + ; isBraidedMonoidal = record + { isMonoidal = Split-IsMF + ; braiding-compat = braiding-compat + } + } -- cgit v1.2.3