From 11e8c93b5426ddfd75f1c9c495e4da0defbc08a6 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 25 Mar 2026 08:53:18 -0500 Subject: Add looped wiring diagrams and merge functor --- Data/WiringDiagram/Equalities.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Data/WiringDiagram/Equalities.agda') diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda index 37b8f38..1e5eb47 100644 --- a/Data/WiringDiagram/Equalities.agda +++ b/Data/WiringDiagram/Equalities.agda @@ -102,7 +102,7 @@ loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identity ≈ ▽ ∘ 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) ∘ α⇒ ∘ △ ⊕₁ 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₂ˡ ⟩ @@ -121,8 +121,8 @@ loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identity ▽ ∘ (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 †)) ⊕₁ 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 -- cgit v1.2.3