Add monoidal structure to system functor

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