diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-15 12:34:15 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-15 12:34:15 -0500 |
| commit | 9a65579633967a0c02b912e6baa3e575a02b868f (patch) | |
| tree | c0398cf53de1b2c0b0e2211bb81f2501c4d8688f /Data/WiringDiagram/Monoidal.agda | |
| parent | 154ad08032f9719b0ad32aa357742fe12ff4899a (diff) | |
Add monoidal structure to system functor
Diffstat (limited to 'Data/WiringDiagram/Monoidal.agda')
| -rw-r--r-- | Data/WiringDiagram/Monoidal.agda | 43 |
1 files changed, 34 insertions, 9 deletions
diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda index 25702e7..d3a6526 100644 --- a/Data/WiringDiagram/Monoidal.agda +++ b/Data/WiringDiagram/Monoidal.agda @@ -189,10 +189,10 @@ module BalancedPush where (g : C ⇒ D) → id-⧈ ⌻ Push.₁ f ⊞₁ Push.₁ g ≈-⧈ Push.₁ (f ×₁ g) ⌻ id-⧈ commute f g = begin - id-⧈ ⌻ Push.₁ f ⊞₁ Push.₁ g ≈⟨ DWD.identityˡ ⟩ - Push.₁ f ⊞₁ Push.₁ g ≈⟨ Push-⊞₁ f g ⟩ - Push.₁ (f ×₁ g) ≈⟨ DWD.identityʳ ⟨ - Push.₁ (f ×₁ g) ⌻ id-⧈ ∎ + id-⧈ ⌻ Push.₁ f ⊞₁ Push.₁ g ≈⟨ DWD.identityˡ ⟩ + Push.₁ f ⊞₁ Push.₁ g ≈⟨ Push-⊞₁ f g ⟩ + Push.₁ (f ×₁ g) ≈⟨ DWD.identityʳ ⟨ + Push.₁ (f ×₁ g) ⌻ id-⧈ ∎ where open DWD.HomReasoning @@ -251,11 +251,16 @@ module BalancedPush where Push.₁ π₁ ≈⟨ Push-π₁ ⟩ unitorʳ⇒ ∎ + Push-swap + : {A B : Obj} + → Push.₁ swap ≈-⧈ swap-⧈ (A □ A) (B □ B) + Push-swap = ∘-resp-≈ˡ swap† ⌸ refl + braiding-compat : {A B : Obj} → Push.₁ (swap {A} {B}) ⌻ id-⧈ ≈-⧈ id-⧈ ⌻ swap-⧈ (A □ A) (B □ B) - braiding-compat = BWD.identityʳ ○ ∘-resp-≈ˡ swap† ⌸ refl ○ BWD.Equiv.sym BWD.identityˡ + braiding-compat = BWD.identityʳ ○ Push-swap ○ BWD.Equiv.sym BWD.identityˡ module BalancedPull where @@ -300,40 +305,60 @@ module BalancedPull where open BWD.HomReasoning open ⇒-Reasoning BWD + Pull-assoc + : {A B C : Obj} + → Pull.₁ (assocʳ {A} {B} {C}) ≈-⧈ associator⇒ + Pull-assoc = refl ⌸ α⇐† + associativity : {A B C : Obj} → Pull.₁ (assocʳ {A} {B} {C}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ associativity = begin Pull.₁ assocʳ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ assocʳ ≈⟨ refl ⌸ α⇐† ⟩ + Pull.₁ assocʳ ≈⟨ Pull-assoc ⟩ assocʳ ∘ π₂ ⧈ assocˡ ≈⟨ introˡ ⊞-identity ⟩ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ ≈⟨ BWD.identityˡ ⟨ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ ∎ + Pull-i₂ + : {A : Obj} + → Pull.₁ (i₂ {𝟘} {A}) ≈-⧈ unitorˡ⇒ + Pull-i₂ = refl ⌸ i₂† + unitaryˡ : {A : Obj} → Pull.₁ (i₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin Pull.₁ i₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ + Pull.₁ i₂ ≈⟨ Pull-i₂ ⟩ unitorˡ⇒ ∎ + Pull-i₁ + : {A : Obj} + → Pull.₁ (i₁ {A} {𝟘}) ≈-⧈ unitorʳ⇒ + Pull-i₁ = refl ⌸ i₁† + unitaryʳ : {A : Obj} → Pull.₁ (i₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin Pull.₁ i₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ + Pull.₁ i₁ ≈⟨ Pull-i₁ ⟩ unitorʳ⇒ ∎ + Pull-swap + : {A B : Obj} + → Pull.₁ swap ≈-⧈ swap-⧈ (A □ A) (B □ B) + Pull-swap = refl ⌸ swap† + braiding-compat : {A B : Obj} → Pull.₁ (swap {A} {B}) ⌻ id-⧈ ≈-⧈ id-⧈ ⌻ swap-⧈ (B □ B) (A □ A) - braiding-compat = BWD.identityʳ ○ refl ⌸ swap† ○ BWD.Equiv.sym BWD.identityˡ + braiding-compat = BWD.identityʳ ○ Pull-swap ○ BWD.Equiv.sym BWD.identityˡ Pulsh-IsMF : IsStrongMonoidalFunctor (S-MC.op ×-⊗ S-MC) DWD-MC Pulsh Pulsh-IsMF = record |