diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-03-25 08:53:18 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-03-25 08:53:18 -0500 |
| commit | 11e8c93b5426ddfd75f1c9c495e4da0defbc08a6 (patch) | |
| tree | 5259224ded58d16a66f47fc3a62a9a1e142fc8eb /Data/WiringDiagram/Equalities.agda | |
| parent | e6de73dd1d40524bc9198096415e99fb45d4432a (diff) | |
Add looped wiring diagrams and merge functor
Diffstat (limited to 'Data/WiringDiagram/Equalities.agda')
| -rw-r--r-- | Data/WiringDiagram/Equalities.agda | 6 |
1 files changed, 3 insertions, 3 deletions
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 |