From 9a65579633967a0c02b912e6baa3e575a02b868f Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 15 Aug 2026 12:34:15 -0500 Subject: Add monoidal structure to system functor --- Data/WiringDiagram/Equalities.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Data/WiringDiagram/Equalities.agda') 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 -- cgit v1.2.3