diff options
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ˡ⇒ |