Add wiring diagram equalitiesmain

4 files changed, 265 insertions, 11 deletions

diff --git a/Data/WiringDiagram/Balanced.agda b/Data/WiringDiagram/Balanced.agda
index 09656fc..ada297b 100644
--- a/Data/WiringDiagram/Balanced.agda
+++ b/Data/WiringDiagram/Balanced.agda
@@ -10,29 +10,78 @@ module Data.WiringDiagram.Balanced
     (S : IdempotentSemiadditiveDagger 𝒞)
   where
 
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
 open import Categories.Functor using (Functor)
-open import Data.WiringDiagram.Core S using (WiringDiagram; _□_)
+open import Data.WiringDiagram.Core S using (WiringDiagram; _□_; _⌸_; push)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Category.Monoidal using (Monoidal)
 open import Data.WiringDiagram.Directed S using (DWD)
-open import Function using (id)
+open import Function using () renaming (id to idf)
 
-open Category 𝒞 using (Obj)
+module 𝒞 = Category 𝒞
+module DWD = Category DWD
 
 -- The category of balanced wiring diagrams
 BWD : Category o ℓ e
 BWD = record
-    { Obj = Obj
+    { Obj = 𝒞.Obj
     ; _⇒_ = λ A B → WiringDiagram (A □ A) (B □ B)
-    ; Category DWD
+    ; DWD
     }
 
 -- Inclusion functor from BWD to DWD
 Include : Functor BWD DWD
 Include = record
     { F₀ = λ A → A □ A
-    ; F₁ = id
+    ; F₁ = idf
     ; identity = Equiv.refl
     ; homomorphism = Equiv.refl
-    ; F-resp-≈ = id
+    ; F-resp-≈ = idf
+    }
+  where
+    open DWD using (module Equiv)
+
+-- Covariant functor from underlying category to BWD
+Push : Functor 𝒞 BWD
+Push = record
+    { F₀ = idf
+    ; F₁ = push
+    ; identity = elimˡ †-identity ⌸ Equiv.refl
+    ; homomorphism = λ {A B C f g} → homoᵢ f g ⌸ Equiv.refl
+    ; F-resp-≈ = λ f≈g → (†-resp-≈ f≈g ⟩∘⟨refl) ⌸ f≈g
     }
   where
-    open Category DWD using (module Equiv)
+    open Category 𝒞
+    open IdempotentSemiadditiveDagger S
+      using (+-monoidal; _†; p₂; _⊕₁_; △; !; p₁; p₂-⊕; ⇒!; ⇒△; ρ⇒≈p₁; p₁∘△; †-homomorphism; †-identity; †-resp-≈)
+    open Monoidal +-monoidal using (assoc-commute-from; unitorˡ-commute-from; triangle)
+    open Shorthands +-monoidal using (α⇒; λ⇒; ρ⇒)
+    open ⇒-Reasoning 𝒞
+    open ⊗-Reasoning +-monoidal
+    homoᵢ
+        : {A B C : Obj}
+          (f : A ⇒ B)
+          (g : B ⇒ C)
+        → (g ∘ f) † ∘ p₂
+        ≈ (f † ∘ p₂) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+    homoᵢ f g = begin
+        (g ∘ f) † ∘ p₂                                                        ≈⟨ pushˡ †-homomorphism ⟩
+        f † ∘ g † ∘ p₂                                                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ p₂-⊕ ⟩
+        f † ∘ g † ∘ λ⇒ ∘ ! ⊕₁ id                                              ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨
+        f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ! ⊕₁ id                                      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ p₁∘△ ⟩⊗⟨refl ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ (p₁ ∘ △ ∘ !) ⊕₁ id                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (ρ⇒≈p₁ ⟩∘⟨refl) ⟩⊗⟨refl ⟨
+        f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ (ρ⇒ ∘ △ ∘ !) ⊕₁ id                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (△ ∘ !) ⊕₁ id                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⇒△ ⟩⊗⟨refl ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ ! ∘ △) ⊕₁ id                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ (g † ∘ λ⇒) ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ (g † ∘ λ⇒) ∘ ! ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        f † ∘ λ⇒ ∘ ! ⊕₁ ((g † ∘ λ⇒) ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullʳ (refl⟩∘⟨ (Equiv.sym ⇒! ⟩⊗⟨refl))) ⟩∘⟨refl ⟩
+        f † ∘ λ⇒ ∘ ! ⊕₁ (g † ∘ λ⇒ ∘ (! ∘ f) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ (pushʳ split₁ˡ)) ⟩∘⟨refl ⟩
+        f † ∘ λ⇒ ∘ ! ⊕₁ (g † ∘ (λ⇒ ∘ ! ⊕₁ id) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullˡ (refl⟩∘⟨ Equiv.sym p₂-⊕)) ⟩∘⟨refl ⟩
+        f † ∘ λ⇒ ∘ ! ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                 ≈⟨ pushʳ (extendʳ (pushʳ serialize₁₂)) ⟩
+        (f † ∘ (λ⇒ ∘ ! ⊕₁ id)) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id  ≈⟨ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl ⟨
+        (f † ∘ p₂) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id              ∎
diff --git a/Data/WiringDiagram/Core.agda b/Data/WiringDiagram/Core.agda
index d2e01cd..9903ce5 100644
--- a/Data/WiringDiagram/Core.agda
+++ b/Data/WiringDiagram/Core.agda
@@ -14,7 +14,7 @@ open import Categories.Category.Monoidal.Utilities using (module Shorthands)
 open import Relation.Binary using (IsEquivalence)
 
 open Category 𝒞 using (Obj; _∘_; _⇒_; id; _≈_; module Equiv)
-open IdempotentSemiadditiveDagger S using (_⊕₀_; _⊕₁_; p₂; +-monoidal; △; ▽)
+open IdempotentSemiadditiveDagger S using (_⊕₀_; _⊕₁_; p₂; +-monoidal; △; ▽; _†)
 open Shorthands +-monoidal using (α⇒)
 
 -- A "Box" is a pair of objects from the underlying category,
@@ -125,6 +125,22 @@ _⌻_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f′ ⧈ g′) (f ⧈ g)
 
 infixr 9 _⌻_
 
--- The loop wiring diagram
+-- Special wiring diagrams
+
 loop : {A : Obj} → WiringDiagram (A □ A) (A □ A)
 loop = ▽ ⧈ id
+
+pulsh : {A B C D : Obj} → A ⇒ B → C ⇒ D → WiringDiagram (B □ C) (A □ D)
+pulsh f g = f ∘ p₂ ⧈ g
+
+push : {A B : Obj} → A ⇒ B → WiringDiagram (A □ A) (B □ B)
+push f = pulsh (f †) f
+
+pull : {A B : Obj} → A ⇒ B → WiringDiagram (B □ B) (A □ A)
+pull f = pulsh f (f †)
+
+merge : {A B : Obj} → A ⇒ B → WiringDiagram (A □ A) (B □ B)
+merge f = f † ∘ ▽ ∘ f ⊕₁ id ⧈ f
+
+split : {A B : Obj} → A ⇒ B → WiringDiagram (B □ B) (A □ A)
+split f = ▽ ∘ id ⊕₁ f ⧈ f †
diff --git a/Data/WiringDiagram/Directed.agda b/Data/WiringDiagram/Directed.agda
index 88c6008..f1cbb93 100644
--- a/Data/WiringDiagram/Directed.agda
+++ b/Data/WiringDiagram/Directed.agda
@@ -17,7 +17,9 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
 open import Categories.Category.Helper using (categoryHelper)
 open import Categories.Category.Monoidal using (Monoidal)
 open import Categories.Category.Monoidal.Utilities using (module Shorthands)
-open import Data.WiringDiagram.Core S using (Box; WiringDiagram; _≈-⧈_; _□_; _⧈_; _⌸_; id-⧈; _⌻_; ≈-isEquiv)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Data.Product using (_,_)
+open import Data.WiringDiagram.Core S using (Box; WiringDiagram; _≈-⧈_; _□_; _⧈_; _⌸_; id-⧈; _⌻_; ≈-isEquiv; pulsh)
 
 open Category 𝒞
 open IdempotentSemiadditiveDagger S
@@ -182,3 +184,37 @@ DWD = categoryHelper record
     ; equiv = ≈-isEquiv
     ; ∘-resp-≈ = ⌻-resp-≈
     }
+
+-- Every pair of morphisms in 𝒞 gives a wiring diagram
+Pulsh : Bifunctor op 𝒞 DWD
+Pulsh = record
+    { F₀ = λ (A , B) → A □ B
+    ; F₁ = λ (f , g) → pulsh f g
+    ; identity = elimˡ Equiv.refl ⌸ Equiv.refl
+    ; homomorphism = λ { {A} {B} {C} {f , g} {f′ , g′} → homoᵢ g g′ f f′ ⌸ Equiv.refl }
+    ; F-resp-≈ = λ (f≈f′ , g≈g′) → (f≈f′ ⟩∘⟨refl) ⌸ g≈g′
+    }
+  where
+    open ⇒-Reasoning 𝒞
+    open ⊗-Reasoning +-monoidal
+    homoᵢ : {A B C D E F : Obj} (g : A ⇒ B) (g′ : B ⇒ C) (f : E ⇒ F) (f′ : D ⇒ E)
+        → (f ∘ f′) ∘ p₂
+        ≈ (f ∘ p₂) ∘ (id ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id)) ∘ α⇒ ∘ (△ ⊕₁ id)
+    homoᵢ g g′ f f′ = begin
+        (f ∘ f′) ∘ p₂                                                     ≈⟨ refl⟩∘⟨ p₂-⊕ ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ ! ⊕₁ id                                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ p₁∘△ ⟩⊗⟨refl  ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ (p₁ ∘ △ ∘ !) ⊕₁ id                                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (ρ⇒≈p₁ ⟩∘⟨refl) ⟩⊗⟨refl ⟨
+        (f ∘ f′) ∘ λ⇒ ∘ (ρ⇒ ∘ △ ∘ !) ⊕₁ id                                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ ⇒△) ⟩⊗⟨refl ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ (ρ⇒ ∘ ! ⊕₁ ! ∘ △) ⊕₁ id                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ʳ ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ ! ∘ △) ⊕₁ id                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ʳ ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ id ⊕₁ λ⇒ ∘ ! ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ (△ ⊕₁ id)          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        (f ∘ f′) ∘ λ⇒ ∘ ! ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id)              ≈⟨ pullʳ (extendʳ (Equiv.sym unitorˡ-commute-from)) ⟩
+        f ∘ λ⇒ ∘ id ⊕₁ f′ ∘ ! ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id)          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        f ∘ λ⇒ ∘ ! ⊕₁ (f′ ∘ λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id)                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩∘⟨ ⇒! ⟩⊗⟨refl) ⟩∘⟨refl ⟨
+        f ∘ λ⇒ ∘ ! ⊕₁ (f′ ∘ λ⇒ ∘ (! ∘ g) ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id)          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pushʳ split₁ˡ) ⟩∘⟨refl ⟩
+        f ∘ λ⇒ ∘ ! ⊕₁ (f′ ∘ (λ⇒ ∘ ! ⊕₁ id) ∘ g ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id)    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ pushˡ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl ⟨
+        f ∘ λ⇒ ∘ ! ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id)              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
+        f ∘ λ⇒ ∘ ! ⊕₁ id ∘ (id ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id)) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ pushʳ (pullˡ (Equiv.sym p₂-⊕)) ⟩
+        (f ∘ p₂) ∘ (id ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id)) ∘ α⇒ ∘ (△ ⊕₁ id)         ∎
diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda
new file mode 100644
index 0000000..37b8f38
--- /dev/null
+++ b/Data/WiringDiagram/Equalities.agda
@@ -0,0 +1,153 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
+open import Level using (Level)
+
+module Data.WiringDiagram.Equalities {o ℓ e : Level} {𝒞 : Category o ℓ e} (S : IdempotentSemiadditiveDagger 𝒞) where
+
+import Categories.Category.Monoidal.Properties as ⊗-Properties
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category.Monoidal using (module Monoidal)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Data.WiringDiagram.Core S using (_⌸_; _⌻_; _≈-⧈_; ≈-trans; loop; push; pull; merge; split)
+
+open Category 𝒞
+open IdempotentSemiadditiveDagger S
+open Monoidal +-monoidal using (module unitorˡ; module unitorʳ; triangle; assoc-commute-from; unitorˡ-commute-from)
+open Shorthands +-monoidal using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐)
+open ⊗-Properties +-monoidal using (coherence₁)
+
+loop∘loop : {A : Obj} → loop ⌻ loop ≈-⧈ loop {A}
+loop∘loop {A} = ≈ᵢ ⌸ identity²
+  where
+    open ⇒-Reasoning 𝒞
+    open ⊗-Reasoning +-monoidal
+    ≈ᵢ : ▽ ∘ id ⊕₁ (▽ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ ▽
+    ≈ᵢ = begin
+        ▽ ∘ id ⊕₁ (▽ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ △ ⊕₁ id              ≈⟨ refl⟩∘⟨ assoc ⟨
+        ▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ △ ⊕₁ id            ≈⟨ extendʳ ▽-assoc ⟨
+        ▽ ∘ ▽ ⊕₁ id ∘ △ ⊕₁ id                   ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩
+        ▽ ∘ (▽ ∘ △) ⊕₁ id                       ≈⟨ refl⟩∘⟨ ▽∘△ ⟩⊗⟨refl ⟩
+        ▽ ∘ id ⊕₁ id                            ≈⟨ elimʳ ⊕.identity ⟩
+        ▽                                       ∎
+
+loop∘push∘loop≈merge : {A B : Obj} (f : A ⇒ B) → id ≤ ((f †) ∘ f) → loop ⌻ push f ⌻ loop ≈-⧈ merge f
+loop∘push∘loop≈merge f id≤f†∘f = ≈ᵢ ⌸ (identityˡ ○ identityʳ)
+  where
+    open ⇒-Reasoning 𝒞
+    open ⊗-Reasoning +-monoidal
+    ≈ᵢ  : (▽ ∘ (id ⊕₁ ((f † ∘ p₂) ∘ id ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ (f ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+        ≈ f † ∘ ▽ ∘ f ⊕₁ id
+    ≈ᵢ = begin
+        (▽ ∘ id ⊕₁ ((f † ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ (f ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id  ≈⟨ (refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl) ⟩∘⟨refl ⟩
+        (▽ ∘ id ⊕₁ (f † ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ (f ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id               ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ (identityʳ ⟩⊗⟨refl)) ⟩∘⟨refl ⟩
+        (▽ ∘ id ⊕₁ (f † ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                      ≈⟨ pushˡ (refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl) ⟩
+        ▽ ∘ (id ⊕₁ (f † ∘ λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id            ≈⟨ refl⟩∘⟨ extendʳ (pullʳ (pullʳ (Equiv.sym serialize₁₂))) ⟩
+        ▽ ∘ id ⊕₁ (f † ∘ λ⇒ ∘ ! ⊕₁ id) ∘ (α⇒ ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id                       ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ (α⇒ ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ (α⇒ ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (pullˡ (Equiv.sym assoc-commute-from)) ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ λ⇒ ∘ (α⇒ ∘ (id ⊕₁ !) ⊕₁ id) ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (pullˡ triangle)  ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ (ρ⇒ ∘ id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ ((ρ⇒ ∘ id ⊕₁ !) ∘ △) ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ △-identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                            ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        ▽ ∘ id ⊕₁ (f † ∘ ▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                                    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ ⇒▽ ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ (f †) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                         ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ merge₁ʳ) ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ (▽ ∘ (f † ∘ f) ⊕₁ (f †)) ∘ α⇒ ∘ △ ⊕₁ id                                               ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        ▽ ∘ id ⊕₁ ▽ ∘ id ⊕₁ (f † ∘ f) ⊕₁ (f †) ∘ α⇒ ∘ △ ⊕₁ id                                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+        ▽ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ (id ⊕₁ (f † ∘ f)) ⊕₁ (f †) ∘ △ ⊕₁ id                                         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩
+        ▽ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ (id ⊕₁ (f † ∘ f) ∘ △) ⊕₁ (f †)                                               ≈⟨ refl⟩∘⟨ sym-assoc ⟩
+        ▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ (id ⊕₁ (f † ∘ f) ∘ △) ⊕₁ (f †)                                             ≈⟨ extendʳ ▽-assoc ⟨
+        ▽ ∘ ▽ ⊕₁ id ∘ (id ⊕₁ (f † ∘ f) ∘ △) ⊕₁ (f †)                                                    ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩
+        ▽ ∘ (id + (f † ∘ f)) ⊕₁ (f †)                                                                   ≈⟨ refl⟩∘⟨ id≤f†∘f ⟩⊗⟨refl ⟩
+        ▽ ∘ (f † ∘ f) ⊕₁ (f †)                                                                          ≈⟨ refl⟩∘⟨ split₁ʳ ⟩
+        ▽ ∘ (f †) ⊕₁ (f †) ∘ f ⊕₁ id                                                                    ≈⟨ extendʳ ⇒▽ ⟨
+        f † ∘ ▽ ∘ f ⊕₁ id                                                                               ∎
+
+merge≈loop∘push : {A B : Obj} (f : A ⇒ B) → merge f ≈-⧈ loop ⌻ push f
+merge≈loop∘push f = ≈ᵢ ⌸ Equiv.sym identityˡ
+  where
+    open ⇒-Reasoning 𝒞
+    open ⊗-Reasoning +-monoidal
+    ≈ᵢ  : f † ∘ ▽ ∘ f ⊕₁ id
+        ≈ (f † ∘ p₂) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+    ≈ᵢ = begin
+        f † ∘ ▽ ∘ f ⊕₁ id                                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ introʳ unitorˡ.isoʳ ⟩⊗⟨refl ⟩
+        f † ∘ ▽ ∘ (f ∘ λ⇒ ∘ λ⇐) ⊕₁ id                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ refl⟩∘⟨ △-identityˡ ) ⟩⊗⟨refl ⟨
+        f † ∘ ▽ ∘ (f ∘ λ⇒ ∘ ! ⊕₁ id ∘ △) ⊕₁ id                      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟩⊗⟨refl ⟨
+        f † ∘ ▽ ∘ (λ⇒ ∘ id ⊕₁ f ∘ ! ⊕₁ id ∘ △) ⊕₁ id                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ pullˡ (Equiv.sym serialize₂₁)) ⟩⊗⟨refl ⟩
+        f † ∘ ▽ ∘ (λ⇒ ∘ ! ⊕₁ f ∘ △) ⊕₁ id                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
+        f † ∘ ▽ ∘ λ⇒ ⊕₁ id ∘ (! ⊕₁ f ∘ △) ⊕₁ id                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
+        f † ∘ ▽ ∘ λ⇒ ⊕₁ id ∘ (! ⊕₁ f) ⊕₁ id ∘ △ ⊕₁ id               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym coherence₁) ⟩
+        f † ∘ ▽ ∘ λ⇒ ∘ α⇒ ∘ (! ⊕₁ f) ⊕₁ id ∘ △ ⊕₁ id                ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨
+        f † ∘ λ⇒ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ (! ⊕₁ f) ⊕₁ id ∘ △ ⊕₁ id          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩
+        f † ∘ λ⇒ ∘ id ⊕₁ ▽ ∘ ! ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        f † ∘ λ⇒ ∘ ! ⊕₁ (▽ ∘ (f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
+        f † ∘ λ⇒ ∘ ! ⊕₁ ▽ ∘ id ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
+        f † ∘ λ⇒ ∘ ! ⊕₁ id ∘ id ⊕₁ ▽ ∘ id ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pushʳ (pullˡ (Equiv.sym p₂-⊕)) ⟩
+        (f † ∘ p₂) ∘ id ⊕₁ ▽ ∘ id ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id         ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        (f † ∘ p₂) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id             ∎
+
+loop∘pull∘loop≈split : {A B : Obj} (f : A ⇒ B) → (f ∘ (f †)) ≤ id → loop ⌻ pull f ⌻ loop ≈-⧈ split f
+loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identityʳ)
+  where
+    open ⇒-Reasoning 𝒞
+    open ⊗-Reasoning +-monoidal
+    ≈ᵢ  : (▽ ∘ (id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id)) ∘ id ⊕₁ (▽ ∘ (f † ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+        ≈ ▽ ∘ id ⊕₁ f
+    ≈ᵢ = begin
+        (▽ ∘ (id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id)) ∘ id ⊕₁ (▽ ∘ (f † ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id  ≈⟨ (refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl) ⟩∘⟨refl ⟩
+        (▽ ∘ (id ⊕₁ (f ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id)) ∘ id ⊕₁ (▽ ∘ (f † ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id               ≈⟨ pullʳ (pullʳ (pullʳ (refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ identityʳ ⟩⊗⟨refl) ⟩∘⟨refl)))⟩ 
+        ▽ ∘ id ⊕₁ (f ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                        ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ p₂ ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ p₂-⊕ ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ triangle ⟩
+        ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩
+        ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ ρ⇐ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩
+        ▽ ∘ id ⊕₁ f ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ ⊕.identity ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                              ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        ▽ ∘ id ⊕₁ (f ∘ ▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                                    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ ⇒▽ ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ (▽ ∘ f ⊕₁ f ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id                                               ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ merge₁ʳ) ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ (▽ ∘ (f ∘ f †) ⊕₁ f) ∘ α⇒ ∘ △ ⊕₁ id                                                     ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        ▽ ∘ id ⊕₁ ▽ ∘ id ⊕₁ (f ∘ f †) ⊕₁ f ∘ α⇒ ∘ △ ⊕₁ id                                                 ≈⟨ refl⟩∘⟨ pushʳ (extendʳ (Equiv.sym assoc-commute-from)) ⟩
+        ▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ (id ⊕₁ (f ∘ f †)) ⊕₁ f ∘ △ ⊕₁ id                                             ≈⟨ extendʳ ▽-assoc ⟨
+        ▽ ∘ ▽ ⊕₁ id ∘ (id ⊕₁ (f ∘ f †)) ⊕₁ f ∘ △ ⊕₁ id                                                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩
+        ▽ ∘ ▽ ⊕₁ id ∘ (id ⊕₁ (f ∘ f †) ∘ △) ⊕₁ f                                                          ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩
+        ▽ ∘ id + (f ∘ f †) ⊕₁ f                                                                           ≈⟨ refl⟩∘⟨ +-commutative ⟩⊗⟨refl ⟩
+        ▽ ∘ (f ∘ f †) + id ⊕₁ f                                                                           ≈⟨ refl⟩∘⟨ f∘f†≤id ⟩⊗⟨refl ⟩
+        ▽ ∘ id ⊕₁ f                                                                                       ∎
+
+split≈pull∘loop : {A B : Obj} (f : A ⇒ B) → split f ≈-⧈ pull f ⌻ loop
+split≈pull∘loop f = ≈ᵢ ⌸ Equiv.sym identityʳ
+  where
+    open ⇒-Reasoning 𝒞
+    open ⊗-Reasoning +-monoidal
+    ≈ᵢ  : ▽ ∘ id ⊕₁ f
+        ≈ ▽ ∘ id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+    ≈ᵢ = begin
+        ▽ ∘ id ⊕₁ f                                             ≈⟨ refl⟩∘⟨ introʳ ⊕.identity ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ id                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟨
+        ▽ ∘ id ⊕₁ f ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ id                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
+        ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ ρ⇐ ⊕₁ id                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityʳ ⟩⊗⟨refl ⟨
+        ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ ! ∘ △) ⊕₁ id            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ ! ∘ △) ⊕₁ id       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ p₂-⊕ ⟩∘⟨refl ⟨
+        ▽ ∘ id ⊕₁ f ∘ id ⊕₁ p₂ ∘ α⇒ ∘ △ ⊕₁ id                   ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩
+        ▽ ∘ id ⊕₁ (f ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id                       ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (pushʳ (introʳ ⊕.identity)) ⟩∘⟨refl ⟩
+        ▽ ∘ id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id          ∎
+
+loop∘push∘loop : {A B : Obj} (f : A ⇒ B) → id ≤ ((f †) ∘ f) → loop ⌻ push f ⌻ loop ≈-⧈ loop ⌻ push f
+loop∘push∘loop f id≤f†∘f = ≈-trans (loop∘push∘loop≈merge f id≤f†∘f) (merge≈loop∘push f)
+
+loop∘pull∘loop : {A B : Obj} → (f : A ⇒ B) → (f ∘ (f †)) ≤ id → loop ⌻ pull f ⌻ loop ≈-⧈ pull f ⌻ loop
+loop∘pull∘loop f f∘f†≤id = ≈-trans (loop∘pull∘loop≈split f f∘f†≤id) (split≈pull∘loop f)