diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/System/Category.agda | 56 | ||||
| -rw-r--r-- | Data/WiringDiagram/Equalities.agda | 5 | ||||
| -rw-r--r-- | Data/WiringDiagram/Monoidal.agda | 43 |
3 files changed, 94 insertions, 10 deletions
diff --git a/Data/System/Category.agda b/Data/System/Category.agda index 50d950b..7e0b791 100644 --- a/Data/System/Category.agda +++ b/Data/System/Category.agda @@ -8,7 +8,10 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Algebra using (CommutativeMonoid) open import Categories.Category using (Category) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Morphism using () renaming (_≅_ to _[_≅_]) open import Data.Setoid using (_⇒ₛ_) +open import Data.Setoid using (∣_∣) open import Data.System.Core using (System; _≤_; ≤-trans; ≤-refl) open import Function using (Func; _⟨$⟩_; flip) open import Relation.Binary as Rel using (Setoid; Rel) @@ -61,3 +64,56 @@ Systems[ I , O ] = record ; equiv = ≈-isEquiv ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i} } + +module _ + {I : Setoid c ℓ} + {O : CommutativeMonoid c ℓ} + {A B : System I O} + (let private module A = System A) + (let private module B = System B) + (≅S : Setoids ℓ ℓ [ A.S ≅ B.S ]) + (let private module O = CommutativeMonoid O) + (let private module ≅S = _[_≅_] ≅S) + (≗-fₛ : (i : ∣ I ∣) (s : ∣ A.S ∣) → ≅S.from ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (≅S.from ⟨$⟩ s)) + (≗-fₒ : (s : ∣ A.S ∣) → (A.fₒ′ s) O.≈ B.fₒ′ (≅S.from ⟨$⟩ s)) + where + + private + + ≗-fₛ-≥ : ((i : ∣ I ∣) (s : ∣ B.S ∣) → ≅S.to ⟨$⟩ (B.fₛ′ i s) A.S.≈ A.fₛ′ i (≅S.to ⟨$⟩ s)) + ≗-fₛ-≥ i s = begin + ≅S.to ⟨$⟩ (B.fₛ′ i s) ≈⟨ cong ≅S.to (cong (B.fₛ ⟨$⟩ i) ≅S.isoʳ) ⟨ + ≅S.to ⟨$⟩ (B.fₛ′ i (≅S.from ⟨$⟩ (≅S.to ⟨$⟩ s))) ≈⟨ cong ≅S.to (≗-fₛ i (≅S.to ⟨$⟩ s)) ⟨ + ≅S.to ⟨$⟩ (≅S.from ⟨$⟩ (A.fₛ′ i (≅S.to ⟨$⟩ s))) ≈⟨ ≅S.isoˡ ⟩ + A.fₛ′ i (≅S.to ⟨$⟩ s) ∎ + where + open ≈-Reasoning A.S + + ≗-fₒ-≥ : (s : ∣ B.S ∣) → B.fₒ′ s O.≈ A.fₒ′ (≅S.to ⟨$⟩ s) + ≗-fₒ-≥ s = begin + B.fₒ′ s ≈⟨ cong B.fₒ ≅S.isoʳ ⟨ + B.fₒ′ (≅S.from ⟨$⟩ (≅S.to ⟨$⟩ s)) ≈⟨ ≗-fₒ (≅S.to ⟨$⟩ s) ⟨ + A.fₒ′ (≅S.to ⟨$⟩ s) ∎ + where + open ≈-Reasoning O.setoid + + A≤B : A ≤ B + A≤B = record + { ⇒S = ≅S.from + ; ≗-fₛ = ≗-fₛ + ; ≗-fₒ = ≗-fₒ + } + + B≤A : B ≤ A + B≤A = record + { ⇒S = ≅S.to + ; ≗-fₛ = ≗-fₛ-≥ + ; ≗-fₒ = ≗-fₒ-≥ + } + + mk-≅ : Systems[ I , O ] [ A ≅ B ] + mk-≅ = record + { from = A≤B + ; to = B≤A + ; iso = record { ≅S } + } 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 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 |