Simplify wiring diagrams using semiadditive daggermain

1 files changed, 70 insertions, 109 deletions

diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda
index 1e5eb47..61deee4 100644
--- a/Data/WiringDiagram/Equalities.agda
+++ b/Data/WiringDiagram/Equalities.agda
@@ -1,150 +1,111 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Categories.Category using (Category)
-open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
+open import Category.Dagger.Semiadditive using (SemiadditiveDagger; 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
+module S = IdempotentSemiadditiveDagger S
+
+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 import Data.WiringDiagram.Core S.semiadditiveDagger using (_⌸_; _⌻_; _≈-⧈_; ≈-trans; loop; push; pull; merge; split)
 
 open Category 𝒞
+
+open Equiv
+open HomReasoning
 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₁)
+open ⇒-Reasoning
+
+⟨π₁,id⟩ : {A B : Obj} → ⟨ π₁ {A} {B} , id ⟩ ≈ assocˡ ∘ Δ ×₁ id
+⟨π₁,id⟩ = begin
+    ⟨ π₁ , id ⟩                   ≈⟨ ⟨⟩-congˡ η ⟨
+    ⟨ π₁ , ⟨ π₁ , π₂ ⟩ ⟩          ≈⟨ assocˡ∘⟨⟩ ⟨
+    assocˡ ∘ ⟨ ⟨ π₁ , π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ Δ∘ identityˡ ⟨
+    assocˡ ∘ Δ ×₁ id              ∎
 
 loop∘loop : {A : Obj} → loop ⌻ loop ≈-⧈ loop {A}
 loop∘loop {A} = ≈ᵢ ⌸ identity²
   where
-    open ⇒-Reasoning 𝒞
-    open ⊗-Reasoning +-monoidal
-    ≈ᵢ : ▽ ∘ id ⊕₁ (▽ ∘ id ⊕₁ 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 ⟩
-        ▽                                       ∎
+        ∇ ∘ ⟨ π₁ , ∇ ∘ id ×₁ id ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ id×₁id) ⟩
+        ∇ ∘ ⟨ id ∘ π₁ , ∇ ∘ id ⟩          ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟨
+        ∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , id ⟩         ≈⟨ refl⟩∘⟨ pushʳ ⟨π₁,id⟩ ⟩
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ Δ ×₁ id  ≈⟨ extendʳ ∇-assoc-×₁ ⟨
+        ∇ ∘ ∇ ×₁ id ∘ Δ ×₁ id             ≈⟨ refl⟩∘⟨ first∘first ⟩
+        ∇ ∘ (∇ ∘ Δ) ×₁ id                 ≈⟨ refl⟩∘⟨ first-cong ∇∘Δ ⟩
+        ∇ ∘ id ×₁ id                      ≈⟨ elimʳ id×₁id ⟩
+        ∇                                 ∎
 
 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
+    ≈ᵢ  : (∇ ∘ ⟨ π₁ , (f † ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f ∘ 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                                                                               ∎
+        (∇ ∘ ⟨ π₁ , (f † ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f ∘ id) ×₁ id ⟩    ≈⟨ pullʳ (⟨⟩-congˡ (elimʳ id×₁id) ⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ first-cong identityʳ)) ⟩
+        ∇ ∘ ⟨ π₁ , f † ∘ π₂ ⟩ ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩                          ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
+        ∇ ∘ ⟨ π₁ ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ , (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ project₂) ⟩
+        ∇ ∘ ⟨ π₁ , f † ∘ ∇ ∘ f ×₁ id ⟩                                        ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (extendʳ ⇒∇-×₁) ⟩
+        ∇ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id ⟩                             ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ×₁∘first) ⟩
+        ∇ ∘ ⟨ π₁ , ∇ ∘ (f † ∘ f) ×₁ (f †) ⟩                                   ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟨
+        ∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , (f † ∘ f) ×₁ (f †) ⟩                             ≈⟨ refl⟩∘⟨ pushʳ (sym assocˡ∘⟨⟩) ⟩
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ (⟨⟩-congʳ identityˡ) ⟨
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ id ∘ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟨
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †)                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-congʳ ×₁∘Δ ⟨
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †)               ≈⟨ extendʳ ∇-assoc-×₁ ⟨
+        ∇ ∘ (∇ ×₁ id) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †)                        ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (id + (f † ∘ f)) ×₁ (f †)                                         ≈⟨ refl⟩∘⟨ ×₁-congʳ id≤f†∘f ⟩
+        ∇ ∘ (f † ∘ f) ×₁ (f †)                                                ≈⟨ refl⟩∘⟨ ×₁∘first ⟨
+        ∇ ∘ (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
+    ≈ᵢ  : f † ∘ ∇ ∘ f ×₁ id ≈ (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ 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             ∎
+        f † ∘ ∇ ∘ f ×₁ id                 ≈⟨ pushʳ (sym project₂)  ⟩
+        (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ 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
+    ≈ᵢ  : (∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f † ∘ 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                                                                                       ∎
+        (∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f † ∘ id) ×₁ id ⟩          ≈⟨ pullʳ (⟨⟩-congˡ (elimʳ id×₁id) ⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ first-cong identityʳ)) ⟩
+        ∇ ∘ ⟨ π₁ , (f ∘ π₂) ⟩ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩                            ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
+        ∇ ∘ ⟨ π₁ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ , (f ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ project₂) ⟩
+        ∇ ∘ ⟨ π₁ , f ∘ ∇ ∘ (f †) ×₁ id ⟩                                            ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (extendʳ ⇒∇-×₁) ⟩
+        ∇ ∘ ⟨ π₁ , ∇ ∘ f ×₁ f ∘ (f †) ×₁ id ⟩                                       ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ×₁∘first) ⟩
+        ∇ ∘ ⟨ π₁ , ∇ ∘ (f ∘ f †) ×₁ f ⟩                                             ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ identityʳ ⟨
+        ∇ ∘ ⟨ π₁ , (∇ ∘ (f ∘ f †) ×₁ f) ∘ id ⟩                                      ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟨
+        ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ ⟨ π₁ , id ⟩                                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ η ⟨
+        ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ ⟨ π₁ , ⟨ π₁ , π₂ ⟩ ⟩                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟨
+        ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ assocˡ ∘ ⟨ ⟨ π₁ , π₁ ⟩ , π₂ ⟩              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ Δ∘ identityˡ ⟨
+        ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ assocˡ ∘ Δ ×₁ id                           ≈⟨ refl⟩∘⟨ pushˡ (sym second∘×₁) ⟩
+        ∇ ∘ id ×₁ ∇ ∘ id ×₁ (f ∘ f †) ×₁ f ∘ assocˡ ∘ Δ ×₁ id                       ≈⟨ refl⟩∘⟨ pushʳ (extendʳ (sym assocˡ∘×₁)) ⟩
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id                   ≈⟨ extendʳ ∇-assoc-×₁ ⟨
+        ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id                              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘first ⟩
+        ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †) ∘ Δ) ×₁ f                                    ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (id + (f ∘ f †)) ×₁ f                                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ (+-comm id (f ∘ f †)) ⟩
+        ∇ ∘ ((f ∘ f †) + id) ×₁ f                                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ f∘f†≤id ⟩
+        ∇ ∘ 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
+    ≈ᵢ  : ∇ ∘ id ×₁ f
+        ≈ ∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ 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          ∎
+        ∇ ∘ id ×₁ f                       ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩
+        ∇ ∘ ⟨ π₁ , f ∘ π₂ ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (introʳ id×₁id) ⟩
+        ∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ 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)