diff options
Diffstat (limited to 'Data/WiringDiagram/Equalities.agda')
| -rw-r--r-- | Data/WiringDiagram/Equalities.agda | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda index 61deee4..1c3928e 100644 --- a/Data/WiringDiagram/Equalities.agda +++ b/Data/WiringDiagram/Equalities.agda @@ -12,7 +12,7 @@ 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.semiadditiveDagger using (_⌸_; _⌻_; _≈-⧈_; ≈-trans; loop; push; pull; merge; split) +open import Data.WiringDiagram.Core S.semiadditiveDagger using (_⌸_; _⌻_; _≈-⧈_; id-⧈; ≈-trans; loop; push; pull; merge; split) open Category 𝒞 @@ -112,3 +112,6 @@ loop∘push∘loop f id≤f†∘f = ≈-trans (loop∘push∘loop≈merge f id 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) + +loop-𝟘 : loop {𝟘} ≈-⧈ id-⧈ +loop-𝟘 = []-unique !-unique₂ π₂∘i₂≈id ⌸ refl |