Construct monoidal merge functor

3 files changed, 242 insertions, 7 deletions

diff --git a/Data/WiringDiagram/Looped.agda b/Data/WiringDiagram/Looped/Core.agda
index 9669e4a..b26f4b7 100644
--- a/Data/WiringDiagram/Looped.agda
+++ b/Data/WiringDiagram/Looped/Core.agda
@@ -7,7 +7,7 @@ open import Category.KaroubiComplete using (KaroubiComplete)
 open import Data.WiringDiagram.Balanced using (BWD)
 open import Level using (Level)
 
-module Data.WiringDiagram.Looped
+module Data.WiringDiagram.Looped.Core
     {o ℓ e o′ ℓ′ e′ : Level}
     {𝒞 : Category o ℓ e}
     {𝒟 : Category o′ ℓ′ e′}
@@ -23,7 +23,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
 
 open import Categories.Category using (Category)
 open import Categories.Functor.Properties using ([_]-resp-∘)
-open import Category.Dagger.2-Poset using (Dagger-2-Poset; dagger-2-poset; Maps; Map)
+open import Category.Dagger.2-Poset using (Dagger-2-Poset; Maps; Map)
 open import Data.WiringDiagram.Balanced S′ using (Include; Push; Pull)
 open import Data.WiringDiagram.Core S′ using (loop; id-⧈; _□_)
 open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘push∘loop; loop∘pull∘loop)
@@ -66,11 +66,14 @@ module _ (A : 𝒞.Obj) where
   l∘forget : L 𝒟.∘ forget 𝒟.≈ forget
   l∘forget = section-absorb
 
+  l∘l : L 𝒟.∘ L 𝒟.≈ L
+  l∘l = [ F ]-resp-∘ loop∘loop
+
 module Push = Functor Push
 module Pull = Functor Pull
 
 S-≤ : Dagger-2-Poset
-S-≤ = dagger-2-poset S
+S-≤ = S.dagger-2-poset
 
 Merge : Functor (Maps S-≤) 𝒟
 Merge = record
diff --git a/Data/WiringDiagram/Looped/Monoidal.agda b/Data/WiringDiagram/Looped/Monoidal.agda
new file mode 100644
index 0000000..d0115ac
--- /dev/null
+++ b/Data/WiringDiagram/Looped/Monoidal.agda
@@ -0,0 +1,214 @@
+{-# 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/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda
index 96ff101..25702e7 100644
--- a/Data/WiringDiagram/Monoidal.agda
+++ b/Data/WiringDiagram/Monoidal.agda
@@ -25,7 +25,7 @@ open import Categories.Morphism.Properties using (id-iso)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
 open import Data.Product using (_,_; zip)
 open import Data.WiringDiagram.Balanced S using (BWD; Push; Pull)
-open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_)
+open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_; loop)
 open import Data.WiringDiagram.Directed S using (DWD; Pulsh)
 open import Data.WiringDiagram.Monoidal.Braided S using (swap-⧈; DWD-Braided) public
 open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public
@@ -207,33 +207,48 @@ module BalancedPush where
   open BWD.HomReasoning
   open ⇒-Reasoning BWD
 
+  Push-assoc
+      : {A B C : Obj}
+      → Push.₁ (assocˡ {A} {B} {C}) ≈-⧈ associator⇒
+  Push-assoc = ∘-resp-≈ˡ α⇒† ⌸ refl
+
   associativity
       : {A B C : Obj}
       → Push.₁ (assocˡ {A} {B} {C}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
       ≈-⧈ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒
   associativity = begin
       Push.₁ assocˡ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
-      Push.₁ assocˡ                       ≈⟨ ∘-resp-≈ˡ α⇒† ⌸ refl ⟩
+      Push.₁ assocˡ                       ≈⟨ Push-assoc ⟩
       assocʳ ∘ π₂ ⧈ assocˡ                ≈⟨ introˡ ⊞-identity ⟩
       id-⧈ ⊞₁ id-⧈ ⌻ associator⇒          ≈⟨ BWD.identityˡ ⟨
       id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒   ∎
 
+  Push-π₂
+      : {A : Obj}
+      → Push.₁ (π₂ {𝟘} {A}) ≈-⧈ unitorˡ⇒
+  Push-π₂ = ∘-resp-≈ˡ π₂† ⌸ refl
+
   unitaryˡ
       : {A : Obj}
       → Push.₁ (π₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
       ≈-⧈ unitorˡ⇒
   unitaryˡ = begin
       Push.₁ π₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
-      Push.₁ π₂                       ≈⟨ ∘-resp-≈ˡ π₂† ⌸ refl ⟩
+      Push.₁ π₂                       ≈⟨ Push-π₂ ⟩
       unitorˡ⇒                        ∎
 
+  Push-π₁
+      : {A : Obj}
+      → Push.₁ (π₁ {A} {𝟘}) ≈-⧈ unitorʳ⇒
+  Push-π₁ = ∘-resp-≈ˡ π₁† ⌸ refl
+
   unitaryʳ
       : {A : Obj}
       → Push.₁ (π₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
       ≈-⧈ unitorʳ⇒
   unitaryʳ = begin
       Push.₁ π₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
-      Push.₁ π₁                       ≈⟨ ∘-resp-≈ˡ π₁† ⌸ refl ⟩
+      Push.₁ π₁                       ≈⟨ Push-π₁ ⟩
       unitorʳ⇒                        ∎
 
   braiding-compat
@@ -391,3 +406,6 @@ Pull-SMF = record
         ; braiding-compat = BalancedPull.braiding-compat
         }
     }
+
+loop⊞loop : {A B : Obj} → loop {A} ⊞₁ loop {B} ≈-⧈ loop
+loop⊞loop = sym S.∇-⊕ ⌸ id×₁id