diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-03 19:08:47 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-03 19:08:47 -0500 |
| commit | 514bb6e3e235f37c4e49bd703ad02a5ab31e8c0a (patch) | |
| tree | ca0b19b2dfda49d0e2ac6c1aa0b87cabca89737e /Data/WiringDiagram/Monoidal.agda | |
| parent | 014e65626daa7bbd0375e5b9ad9bf0ad8addabdc (diff) | |
Show category of maps is monoidal
Diffstat (limited to 'Data/WiringDiagram/Monoidal.agda')
| -rw-r--r-- | Data/WiringDiagram/Monoidal.agda | 38 |
1 files changed, 15 insertions, 23 deletions
diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda index 3d7ea78..96ff101 100644 --- a/Data/WiringDiagram/Monoidal.agda +++ b/Data/WiringDiagram/Monoidal.agda @@ -28,7 +28,7 @@ open import Data.WiringDiagram.Balanced S using (BWD; Push; Pull) open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_) open import Data.WiringDiagram.Directed S using (DWD; Pulsh) open import Data.WiringDiagram.Monoidal.Braided S using (swap-⧈; DWD-Braided) public -open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; σ₂₃; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public +open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public open import Data.WiringDiagram.Monoidal.Symmetric S using (DWD-Symmetric; BWD-Symmetric) public module DWD = Category DWD @@ -141,23 +141,19 @@ module Directed where unitaryˡ : {A B : Obj} - → Pulsh.₁ (⟨ ! {A} , id {A} ⟩ , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pulsh.₁ (i₂ {𝟘} {A} , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin - Pulsh.₁ (⟨ ! , id ⟩ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pulsh.₁ (⟨ ! , id ⟩ , π₂) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒) , refl) ⟩ - Pulsh.₁ (⟨ zero⇒ , id ⟩ , π₂) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id , refl) ⟩ - unitorˡ⇒ ∎ + Pulsh.₁ (i₂ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + unitorˡ⇒ ∎ unitaryʳ : {A B : Obj} - → Pulsh.₁ (⟨ id {A} , ! {A} ⟩ , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pulsh.₁ (i₁ {A} {𝟘} , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin - Pulsh.₁ (⟨ id , ! ⟩ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pulsh.₁ (⟨ id , ! ⟩ , π₁) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒) , refl) ⟩ - Pulsh.₁ (⟨ id , zero⇒ ⟩ , π₁) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0 , refl) ⟩ - unitorʳ⇒ ∎ + Pulsh.₁ (i₁ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + unitorʳ⇒ ∎ braiding-compat : {A B C D : Obj} @@ -302,25 +298,21 @@ module BalancedPull where unitaryˡ : {A : Obj} - → Pull.₁ ⟨ ! {A} , id {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pull.₁ (i₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin - Pull.₁ ⟨ ! , id ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ ⟨ ! , id ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒)) ⟩ - Pull.₁ ⟨ zero⇒ , id ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id) ⟩ - Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ - unitorˡ⇒ ∎ + Pull.₁ i₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ + unitorˡ⇒ ∎ unitaryʳ : {A : Obj} - → Pull.₁ ⟨ id {A} , ! {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pull.₁ (i₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin - Pull.₁ ⟨ id , ! ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ ⟨ id , ! ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒)) ⟩ - Pull.₁ ⟨ id , zero⇒ ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0) ⟩ - Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ - unitorʳ⇒ ∎ + Pull.₁ i₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ + unitorʳ⇒ ∎ braiding-compat : {A B : Obj} |