Finish merge and split symmetric monoidal functors

1 files changed, 242 insertions, 0 deletions

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
+        }
+    }