diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-31 20:52:41 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-31 20:52:41 -0700 |
| commit | f70dd41bf5a519ba099ebd6d9a425a022c1a111f (patch) | |
| tree | 399fc3dd769b739614fc43e561bbc83c01815ae4 /Data/WiringDiagram/Monoidal/Core.agda | |
| parent | 02b36f31cac4c2e530e496e7cc9154abef94ddfc (diff) | |
Show wiring diagram braiding is symmetric
Diffstat (limited to 'Data/WiringDiagram/Monoidal/Core.agda')
| -rw-r--r-- | Data/WiringDiagram/Monoidal/Core.agda | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Data/WiringDiagram/Monoidal/Core.agda b/Data/WiringDiagram/Monoidal/Core.agda index 382e188..5abd60f 100644 --- a/Data/WiringDiagram/Monoidal/Core.agda +++ b/Data/WiringDiagram/Monoidal/Core.agda @@ -483,6 +483,8 @@ module Directed where open Morphism DWD using (_≅_) + -- Monoidal product bifunctor + -⊞- : Bifunctor DWD DWD DWD -⊞- = record { F₀ = uncurry′ _⊞_ @@ -492,6 +494,8 @@ module Directed where ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈ } + -- Structure isomorphisms + unitorˡ : {X : Box} → 𝟘-□ ⊞ X ≅ X unitorˡ {X} = record { from = unitorˡ⇒ @@ -532,6 +536,8 @@ module Balanced where open Morphism BWD using (_≅_) + -- Monoidal product bifunctor + -⊞- : Bifunctor BWD BWD BWD -⊞- = record { F₀ = uncurry′ _⊕_ @@ -541,6 +547,8 @@ module Balanced where ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈ } + -- Structure isomorphisms + unitorˡ : {X : Obj} → 𝟘 ⊕ X ≅ X unitorˡ {X} = record { from = unitorˡ⇒ |