From 9a65579633967a0c02b912e6baa3e575a02b868f Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 15 Aug 2026 12:34:15 -0500 Subject: Add monoidal structure to system functor --- Category/Dagger/Semiadditive.agda | 44 ++- Data/System/Category.agda | 56 +++ Data/WiringDiagram/Equalities.agda | 5 +- Data/WiringDiagram/Monoidal.agda | 43 ++- Functor/Instance/WiringDiagram/System.agda | 70 +++- .../Monoidal/Instance/WiringDiagram/System.agda | 422 +++++++++++++++++++++ 6 files changed, 621 insertions(+), 19 deletions(-) create mode 100644 Functor/Monoidal/Instance/WiringDiagram/System.agda diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index adcf6ed..41be19e 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -11,8 +11,11 @@ import Category.Semiadditive.Monoidal as SemiadditiveMonoidal open import Categories.Category.Dagger using (HasDagger) open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Braided using (Braided) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) -open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor) open import Categories.Morphism using (Iso) open import Categories.Morphism.Properties 𝒞 using (Iso-resp-≈; Iso-swap) open import Category.Dagger.2-Poset using (Dagger-2-Poset; Map; Maps; unitary-isMap) @@ -272,9 +275,10 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where maps = Maps dagger-2-poset open Dagger-2-Poset dagger-2-poset using (category) - open SemiadditiveMonoidal semiadditive using (monoidal) + open SemiadditiveMonoidal semiadditive using (monoidal; symmetric) module M = Monoidal monoidal + module SM = Symmetric symmetric ×₁-functional : {A B C D : Obj} @@ -392,8 +396,44 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where ; M } + swap-unitary : {X Y : Obj} → Iso category (swap {X} {Y}) (swap †) + swap-unitary {X} {Y} = record { Iso (Iso-resp-≈ (SM.braiding.iso (X , Y)) refl (sym swap†)) } + + swap-map : {X Y : Obj} → Map dagger-2-poset (X ⊕ Y) (Y ⊕ X) + swap-map = record + { map = swap + ; isMap = unitary-isMap dagger-2-poset swap-unitary + } + + σ : ⊗ ≃ flip-bifunctor ⊗ + σ = niHelper record + { η = λ _ → swap-map + ; η⁻¹ = λ _ → swap-map + ; commute = λ _ → swap∘×₁ + ; iso = λ X → record { SM.braiding.iso X } + } + + maps-braided : Braided maps-monoidal + maps-braided = record + { braiding = σ + ; SM + } + + maps-symmetric : Symmetric maps-monoidal + maps-symmetric = record + { braided = maps-braided + ; SM + } + maps-MC : MonoidalCategory o (ℓ ⊔ e) e maps-MC = record { U = maps ; monoidal = maps-monoidal } + + maps-SMC : SymmetricMonoidalCategory o (ℓ ⊔ e) e + maps-SMC = record + { U = maps + ; monoidal = maps-monoidal + ; symmetric = maps-symmetric + } 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 diff --git a/Functor/Instance/WiringDiagram/System.agda b/Functor/Instance/WiringDiagram/System.agda index 80a4fe5..891787b 100644 --- a/Functor/Instance/WiringDiagram/System.agda +++ b/Functor/Instance/WiringDiagram/System.agda @@ -11,7 +11,7 @@ open import Category.Instance.CMonoids using (CMonoids; CMonoidHomomorphism) open import Level using (Level; suc) module Functor.Instance.WiringDiagram.System - {o ℓ e o′ ℓ′ e′ : Level} + {o ℓ e : Level} {c : Level} {𝒞 : Category o ℓ e} {S : IdempotentSemiadditiveDagger 𝒞} @@ -24,6 +24,7 @@ import Data.System.Monoidal as Sys-⊗ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Algebra using (CommutativeMonoid) +open import Algebra.Construct.DirectProduct using () renaming (commutativeMonoid to _×ₘ_) open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.CartesianClosed using (CartesianClosed) open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-CCC) @@ -32,6 +33,8 @@ open import Categories.Category.Product using (_⁂_) open import Categories.Functor.Cartesian.Properties using (isMonoidalFunctor) open import Categories.Functor.Monoidal using (MonoidalFunctor) open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Categories.Morphism using (module ≅) open import Categories.Morphism.Reasoning.Iso (CMonoids c c) using (switch-fromtoˡ) open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) open import Categories.Object.Product (CMonoids c c) using (Product; IsProduct) @@ -94,6 +97,61 @@ _⟦⊕⟧_ {A} {B} a b = ⟦ F.×-iso.to A B ⟧ (a , b) ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F module ⊗-F = MonoidalFunctor ⊗-F +⟦⊕⟧-assocˡ + : {A B C : Obj} + (a : Carrier (F.₀ A)) + (b : Carrier (F.₀ B)) + (c : Carrier (F.₀ C)) + → (let open CommutativeMonoid (F.₀ (A ⊕ (B ⊕ C))) using (_≈_)) + → ⟦ F.₁ S.assocˡ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c) ≈ a ⟦⊕⟧ (b ⟦⊕⟧ c) +⟦⊕⟧-assocˡ {A} {B} {C} a b c- = begin + ⟦ F.₁ S.assocˡ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c-) ≈⟨ ⊗-F.associativity ((a , b) , c-) ⟩ + a ⟦⊕⟧ (b ⟦⊕⟧ c-) ∎ + where + open ≈-Reasoning (setoid (F.₀ (A ⊕ (B ⊕ C)))) + module 𝒞-CC = CartesianCategory 𝒞-CC + ⊗-F : MonoidalFunctor 𝒞-CC.monoidalCategory (CMonoids-CC.monoidalCategory {c} {c}) + ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F + module ⊗-F = MonoidalFunctor ⊗-F + +⟦⊕⟧-assocʳ + : {A B C : Obj} + (a : Carrier (F.₀ A)) + (b : Carrier (F.₀ B)) + (c : Carrier (F.₀ C)) + → (let open CommutativeMonoid (F.₀ ((A ⊕ B) ⊕ C)) using (_≈_)) + → ⟦ F.₁ S.assocʳ ⟧ (a ⟦⊕⟧ (b ⟦⊕⟧ c)) ≈ (a ⟦⊕⟧ b) ⟦⊕⟧ c +⟦⊕⟧-assocʳ {A} {B} {C} a b c- = begin + ⟦ F.₁ S.assocʳ ⟧ (a ⟦⊕⟧ (b ⟦⊕⟧ c-)) ≈⟨ switch-fromtoˡ ([ F.F ]-resp-≅ (≅.sym 𝒞 S.⊕-assoc)) {h = h} {k = k} ⊗-F.associativity ((a , b) , c-) ⟨ + (a ⟦⊕⟧ b) ⟦⊕⟧ c- ∎ + where + open ≈-Reasoning (setoid (F.₀ ((A ⊕ B) ⊕ C))) + module 𝒞-CC = CartesianCategory 𝒞-CC + ⊗-F : MonoidalFunctor 𝒞-CC.monoidalCategory (CMonoids-CC.monoidalCategory {c} {c}) + ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F + module ⊗-F = MonoidalFunctor ⊗-F + h : CMonoidHomomorphism c c ((F.₀ A ×ₘ F.₀ B) ×ₘ F.₀ C) (F.₀ ((A ⊕ B) ⊕ C)) + h = ⊗-F.⊗-homo.η (A ⊕ B , C) CMonoids-CC.∘ (⊗-F.⊗-homo.η (A , B) CMonoids-CC.×₁ CMonoids-CC.id) + k : CMonoidHomomorphism c c ((F.₀ A ×ₘ F.₀ B) ×ₘ F.₀ C) (F.₀ (A ⊕ (B ⊕ C))) + k = ⊗-F.⊗-homo.η (A , B ⊕ C) CMonoids-CC.∘ (CMonoids-CC.id CMonoids-CC.×₁ ⊗-F.⊗-homo.η (B , C)) CMonoids-CC.∘ CMonoids-CC.assocˡ + +⟨⟩-⟦⊕⟧ + : {A B C : Obj} + {f : A ⇒ B} + {g : A ⇒ C} + (a : Carrier (F.₀ A)) + → (let open CommutativeMonoid (F.₀ (B ⊕ C)) using (_≈_)) + → ⟦ F.₁ S.⟨ f , g ⟩ ⟧ a ≈ ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ a +⟨⟩-⟦⊕⟧ {A} {B} {C} {f} {g} a = begin + ⟦ F.₁ S.⟨ f , g ⟩ ⟧ a ≈⟨ switch-fromtoˡ (F.×-iso B C) {h = h} {k = k} (F.F-resp-⟨⟩ f g) a ⟩ + ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ a ∎ + where + h : CMonoidHomomorphism c c (F.₀ A) (F.₀ (B ⊕ C)) + h = F.₁ S.⟨ f , g ⟩ + k : CMonoidHomomorphism c c (F.₀ A) _ + k = CMonoids-CC.⟨ F.₁ f , F.₁ g ⟩ + open ≈-Reasoning (setoid (F.₀ (B ⊕ C))) + ⟦⊕⟧-congˡ : {A B : Obj} (let module FB = CommutativeMonoid (F.₀ B)) @@ -243,14 +301,10 @@ homomorphism {Xᵢ} {Xₒ} {Yᵢ} {Yₒ} {Zᵢ} {Zₒ} {fᵢ} {fₒ} {gᵢ} {g → ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈ X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) lem₂ = begin - ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ switch-fromtoˡ (F.×-iso Xₒ (Xₒ ⊕ Zᵢ)) {h = h} {k = k} (F.F-resp-⟨⟩ S.π₁ 𝒞.id) (X.fₒ′ s ⟦⊕⟧ i) ⟩ - ⟦ F.₁ S.π₁ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟦⊕⟧-cong (F.F-resp-×.project₁ (X.fₒ′ s , i)) (F.identity (X.fₒ′ s ⟦⊕⟧ i)) ⟩ + ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟨⟩-⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ S.π₁ ⟧ _ ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟦⊕⟧-cong (F.F-resp-×.project₁ (X.fₒ′ s , i)) (F.identity (X.fₒ′ s ⟦⊕⟧ i)) ⟩ X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) ∎ where - h : CMonoidHomomorphism c c (F.₀ (Xₒ ⊕ Zᵢ)) (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ))) - h = F.₁ _ - k : CMonoidHomomorphism c c (F.₀ (Xₒ ⊕ Zᵢ)) _ - k = CMonoids-CC.⟨ F.₁ _ , F.₁ _ ⟩ open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ)))) lem₃ : (let open CommutativeMonoid (F.₀ (Xₒ ⊕ Yᵢ)) using (_≈_)) @@ -341,3 +395,5 @@ Sys = record ; homomorphism = homomorphism ; F-resp-≈ = Sys-resp-≈ } + +module Sys = Functor Sys diff --git a/Functor/Monoidal/Instance/WiringDiagram/System.agda b/Functor/Monoidal/Instance/WiringDiagram/System.agda new file mode 100644 index 0000000..786b221 --- /dev/null +++ b/Functor/Monoidal/Instance/WiringDiagram/System.agda @@ -0,0 +1,422 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Categories.Category using (Category) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Category.Instance.Cats using (Cats) +open import Categories.Functor using (Functor; _∘F_) renaming (id to IdF) +open import Categories.Functor.Cartesian using (CartesianF) +open import Category.Cartesian.Instance.CMonoids using (CMonoids-CC) +open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.Instance.CMonoids using (CMonoids; CMonoidHomomorphism) +open import Level using (Level; suc) + +module Functor.Monoidal.Instance.WiringDiagram.System + {o ℓ e o′ ℓ′ e′ : Level} + {c : Level} + {𝒞 : Category o ℓ e} + {S : IdempotentSemiadditiveDagger 𝒞} + (let private module S = IdempotentSemiadditiveDagger S) + (let 𝒞-CC = record { cartesian = S.cartesian }) + (F : CartesianF 𝒞-CC (CMonoids-CC {c} {c})) + where + +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra using (CommutativeMonoid) +open import Algebra.Construct.DirectProduct using () renaming (commutativeMonoid to _×ₘ_) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) +open import Categories.Category.CartesianClosed using (CartesianClosed) +open import Categories.Category.Instance.Cats using (Cats) +open import Categories.Category.Instance.One using (One) +open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-CCC) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory) +open import Categories.Category.Monoidal.Instance.Cats using (module Product) +open import Categories.Category.Product using (_※_; _⁂_; πˡ; πʳ) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.Functor.Monoidal using (IsMonoidalFunctor; MonoidalFunctor) +open import Categories.Morphism using (module ≅) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso) +open import Data.Product using (_,_) +open import Data.Product using (proj₁; proj₂) +open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) +open import Data.System using (discrete; ≤-refl; System; _≤_; mk-≅) +open import Data.Unit.Polymorphic using (tt) +open import Data.WiringDiagram.Core S.semiadditiveDagger using (Box; _□_; WiringDiagram) +open import Data.WiringDiagram.Monoidal S.semiadditiveDagger using (DWD-MC) +open import Data.WiringDiagram.Monoidal.Core S.semiadditiveDagger using (𝟘-□; _⊞_; _⊞₁_; module Directed) +open import Function using (_⟨$⟩_; Func) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) +open import Functor.Instance.WiringDiagram.System {S = S} F using (wire; Sys; _⟦⊕⟧_; ⟦⊕⟧-cong; ⟦⊕⟧-congˡ; ⟦⊕⟧-commute; ⟦⊕⟧-assocˡ; ⟦⊕⟧-assocʳ; ⟨⟩-⟦⊕⟧; Wire) +open import Relation.Binary using (Setoid) + +module F = CartesianF F +module Setoids-CC = CartesianClosed (Setoids-CCC c) + +open CMonoidHomomorphism using (⟦_⟧; func; ⟦⟧-cong) +open Cartesian Setoids-CC.cartesian using (×-assoc; assocˡ; assocʳ) +open Category 𝒞 hiding (_≈_) +open CommutativeMonoid using (setoid; Carrier) +open Directed using (-⊞-) +open S using (_⊕_; _×₁_; σ₂₃) + +Cats-MC : MonoidalCategory (suc (suc c)) (suc c) (suc c) +Cats-MC = record + { U = Cats (suc c) c c + ; monoidal = Product.Cats-Monoidal + } + +module Cats-MC = MonoidalCategory Cats-MC +module Cats-C = Cartesian Product.Cats-is + +ε : Functor (One {suc c} {c} {c}) (Sys.₀ 𝟘-□) +ε = record + { F₀ = λ _ → discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘) + ; F₁ = λ _ → ≤-refl + ; identity = tt + ; homomorphism = tt + ; F-resp-≈ = λ _ → tt + } + +×-System + : {A B C D : Obj} + → System (setoid (F.₀ A)) (F.₀ B) + → System (setoid (F.₀ C)) (F.₀ D) + → System (setoid (F.₀ (A ⊕ C))) (F.₀ (B ⊕ D)) +×-System {A} {B} {C} {D} X Y = record + { S = X.S ×ₛ Y.S + ; fₛ = λg (< eval ∙ (X.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Y.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ) ∙ func (F.×-iso.from A C) + ; fₒ = func (F.×-iso.to B D) ∙ X.fₒ ×-function Y.fₒ + } + where + module X = System X + module Y = System Y + open CartesianClosed (Setoids-CCC c) using (λg; eval; cartesian) + open Cartesian cartesian using (π₁; π₂; ⟨_,_⟩) + +≤-×-System + : {A B C D : Obj} + {X X′ : System (setoid (F.₀ A)) (F.₀ B)} + {Y Y′ : System (setoid (F.₀ C)) (F.₀ D)} + → X ≤ X′ + → Y ≤ Y′ + → ×-System X Y ≤ ×-System X′ Y′ +≤-×-System {A} {B} {C} {D} {X} {X′} {Y} {Y′} ≤X ≤Y = record + { ⇒S = ≤X.⇒S ×-function ≤Y.⇒S + ; ≗-fₛ = λ i (s₁ , s₂) → ≤X.≗-fₛ (⟦ F.₁ S.π₁ ⟧ i) s₁ , ≤Y.≗-fₛ (⟦ F.₁ S.π₂ ⟧ i) s₂ + ; ≗-fₒ = λ (s₁ , s₂) → ⟦⊕⟧-cong (≤X.≗-fₒ s₁) (≤Y.≗-fₒ s₂) + } + where + module ≤X = _≤_ ≤X + module ≤Y = _≤_ ≤Y + module X = System X + module Y = System Y + module X′ = System X′ + module Y′ = System Y′ + module X⊗Y = System (×-System X Y) + module X⊗Y′ = System (×-System X′ Y′) + open CommutativeMonoid (F.₀ (B ⊕ D)) using (_≈_) + +η : (X Y : Box) → Bifunctor (Sys.₀ X) (Sys.₀ Y) (Sys.₀ (X ⊞ Y)) +η X Y = record + { F₀ = λ (x , y) → ×-System x y + ; F₁ = λ (f , g) → ≤-×-System f g + ; identity = λ {(A , B)} → S.refl A , S.refl B + ; homomorphism = λ {_ _ (Z , Z′)} → S.refl Z , S.refl Z′ + ; F-resp-≈ = λ (≈f , ≈g) → ≈f , ≈g + } + where + open System using (S) + +module Commute + {A A′ B B′ C C′ D D′ : Obj} + (f : WiringDiagram (A □ B) (A′ □ B′)) + (g : WiringDiagram (C □ D) (C′ □ D′)) + (X : System (setoid (F.₀ A)) (F.₀ B)) + (Y : System (setoid (F.₀ C)) (F.₀ D)) + where + open WiringDiagram + fᵢ : B ⊕ A′ ⇒ A + fᵢ = input f + fₒ : B ⇒ B′ + fₒ = output f + gᵢ : D ⊕ C′ ⇒ C + gᵢ = input g + gₒ : D ⇒ D′ + gₒ = output g + module X = System X + module Y = System Y + module X⊗Y = System (×-System X Y) + module B⊗D = CommutativeMonoid (F.₀ (B′ ⊕ D′)) + open System using (fₛ′; fₒ′) + module _ (s : ∣ X⊗Y.S ∣) where + open CartesianClosed (Setoids-CCC c) using (λg; eval) + open Func using (cong) + s₁ : ∣ X.S ∣ + s₁ = proj₁ s + s₂ : ∣ Y.S ∣ + s₂ = proj₂ s + ≗-fₛ + : (i : Carrier (F.₀ (A′ ⊕ C′))) + → (fₛ′ (wire fᵢ fₒ X) (⟦ F.₁ S.π₁ ⟧ i) s₁ , fₛ′ (wire gᵢ gₒ Y) (⟦ F.₁ S.π₂ ⟧ i) s₂) + X⊗Y.S.≈ X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ i)) (s₁ , s₂) + ≗-fₛ i = let open ≈-Reasoning X⊗Y.S in begin + X.fₛ′ (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ i₁)) s₁ , Y.fₛ′ (⟦ F.₁ gᵢ ⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂)) s₂ + ≈⟨ cong + (λg (< eval ∙ (X.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Y.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ)) + (F.×-iso.isoʳ A C (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ i₁) , ⟦ F.₁ gᵢ ⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂))) ⟨ + X⊗Y.fₛ′ (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ i₁) ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂)) (s₁ , s₂) + ≈⟨ cong X⊗Y.fₛ (⟦⊕⟧-commute (X.fₒ′ s₁ ⟦⊕⟧ i₁) (Y.fₒ′ s₂ ⟦⊕⟧ i₂)) ⟨ + X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ i₁) ⟦⊕⟧ (Y.fₒ′ s₂ ⟦⊕⟧ i₂))) (s₁ , s₂) + ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ)) + (⟦⊕⟧-cong + (⟦⊕⟧-cong (F.F-resp-×.project₁ (X.fₒ′ s₁ , Y.fₒ′ s₂)) (F.F-resp-×.project₁ (i₁ , i₂))) + (⟦⊕⟧-cong (F.F-resp-×.project₂ (X.fₒ′ s₁ , Y.fₒ′ s₂)) (F.F-resp-×.project₂ (i₁ , i₂))))) ⟨ + X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧ + (((⟦ F.₁ S.π₁ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂)) ⟦⊕⟧ (⟦ F.₁ S.π₁ ⟧ (i₁ ⟦⊕⟧ i₂))) ⟦⊕⟧ + ((⟦ F.₁ S.π₂ ⟧ (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂)) ⟦⊕⟧ (⟦ F.₁ S.π₂ ⟧ (i₁ ⟦⊕⟧ i₂))))) (s₁ , s₂) + ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ)) + (⟦⊕⟧-cong + (⟦⊕⟧-commute (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) (i₁ ⟦⊕⟧ i₂)) + (⟦⊕⟧-commute (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) (i₁ ⟦⊕⟧ i₂)))) ⟨ + X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧ + ((⟦ F.₁ (S.π₁ ×₁ S.π₁) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))) ⟦⊕⟧ + (⟦ F.₁ (S.π₂ ×₁ S.π₂) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))))) (s₁ , s₂) + ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ)) (⟨⟩-⟦⊕⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂)))) ⟨ + X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ) ⟧ (⟦ F.₁ σ₂₃ ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂)))) (s₁ , s₂) + ≈⟨ cong X⊗Y.fₛ (F.homomorphism ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))) ⟨ + X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃) ⟧ (_ ⟦⊕⟧ (i₁ ⟦⊕⟧ i₂))) (s₁ , s₂) + ≈⟨ cong X⊗Y.fₛ (⟦⟧-cong (F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃)) (⟦⊕⟧-congˡ (F.×-iso.isoˡ A′ C′ i))) ⟩ + X⊗Y.fₛ′ (⟦ F.₁ (fᵢ ×₁ gᵢ ∘ σ₂₃) ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ i)) (s₁ , s₂) + ∎ + where + i₁ : Carrier (F.₀ A′) + i₁ = proj₁ (⟦ F.×-iso.from A′ C′ ⟧ i) + i₂ : Carrier (F.₀ C′) + i₂ = proj₂ (⟦ F.×-iso.from A′ C′ ⟧ i) + ≗-fₒ + : fₒ′ (×-System (wire fᵢ fₒ X) (wire gᵢ gₒ Y)) (s₁ , s₂) + B⊗D.≈ fₒ′ (wire (fᵢ ×₁ gᵢ ∘ σ₂₃) (fₒ ×₁ gₒ) (×-System X Y)) (s₁ , s₂) + ≗-fₒ = let open ≈-Reasoning B⊗D.setoid in begin + ⟦ F.₁ fₒ ⟧ (X.fₒ′ s₁) ⟦⊕⟧ ⟦ F.₁ gₒ ⟧ (Y.fₒ′ s₂) ≈⟨ ⟦⊕⟧-commute (X.fₒ′ s₁) (Y.fₒ′ s₂) ⟨ + ⟦ F.₁ (fₒ ×₁ gₒ) ⟧ (X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ∎ + +commute + : {A B C D : Box} + (f : WiringDiagram A C) + (g : WiringDiagram B D) + (let fᵢ = WiringDiagram.input f) + (let gᵢ = WiringDiagram.input g) + (let fₒ = WiringDiagram.output f) + (let gₒ = WiringDiagram.output g) + → η C D ∘F (Wire fᵢ fₒ ∘F πˡ ※ Wire gᵢ gₒ ∘F πʳ) + ≃ Wire (fᵢ ×₁ gᵢ ∘ σ₂₃) (fₒ ×₁ gₒ) ∘F η A B +commute f g = + pointwise-iso + (λ (X , Y) → mk-≅ (≅.refl (Setoids c c)) (λ i s → Commute.≗-fₛ f g X Y s i) (Commute.≗-fₒ f g X Y)) + (λ { {X , Y} {X′ , Y′} (h , i) → S.refl X′ , S.refl Y′ }) + where + open System + +⊗-homo : NaturalTransformation (Cats-C.-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -⊞-) +⊗-homo = ntHelper record + { η = λ (X , Y) → η X Y + ; commute = λ { {A , B} {C , D} (f , g) → commute f g } + } + +module Associativity + {A A′ B B′ C C′ : Obj} + (X : System (setoid (F.₀ A)) (F.₀ A′)) + (Y : System (setoid (F.₀ B)) (F.₀ B′)) + (Z : System (setoid (F.₀ C)) (F.₀ C′)) where + + module X = System X + module Y = System Y + module Z = System Z + + module X⊗Y = System (×-System X Y) + module [X⊗Y]⊗Z = System (×-System (×-System X Y) Z) + module X⊗[Y⊗Z] = System (×-System X (×-System Y Z)) + + open System + + module _ (s : ∣ (X.S ×ₛ Y.S) ×ₛ Z.S ∣) where + open Setoid X⊗[Y⊗Z].S using (_≈_) + + s₁ : ∣ X.S ∣ + s₁ = proj₁ (proj₁ s) + s₂ : ∣ Y.S ∣ + s₂ = proj₂ (proj₁ s) + s₃ : ∣ Z.S ∣ + s₃ = proj₂ s + + ≗-fₛ + : (i : Carrier (F.₀ (A ⊕ (B ⊕ C)))) + → assocˡ {X.S} {Y.S} {Z.S} ⟨$⟩ System.fₛ′ (wire (S.assocʳ ∘ S.π₂) S.assocˡ (×-System (×-System X Y) Z)) i s + ≈ X⊗[Y⊗Z].fₛ′ i (assocˡ {X.S} {Y.S} {Z.S} ⟨$⟩ s) + ≗-fₛ i = begin + assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ (S.assocʳ ∘ S.π₂) ⟧ ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) ⟦⊕⟧ i)) ((s₁ , s₂) , s₃) + ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (F.homomorphism ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) ⟦⊕⟧ i))) ⟩ + assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ (⟦ F.₁ S.π₂ ⟧ ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) ⟦⊕⟧ i))) ((s₁ , s₂) , s₃) + ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⟧-cong (F.₁ S.assocʳ) (F.F-resp-×.project₂ ([X⊗Y]⊗Z.fₒ′ ((s₁ , s₂) , s₃) , i)))) ⟩ + assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ i) ((s₁ , s₂) , s₃) + ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⟧-cong (F.₁ S.assocʳ) (F.×-iso.isoˡ A (B ⊕ C) i))) ⟨ + assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ (i₁ ⟦⊕⟧ i₂₃)) ((s₁ , s₂) , s₃) + ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⟧-cong (F.₁ S.assocʳ) (⟦⊕⟧-congˡ (F.×-iso.isoˡ B C i₂₃)))) ⟨ + assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ (⟦ F.₁ S.assocʳ ⟧ (i₁ ⟦⊕⟧ (i₂ ⟦⊕⟧ i₃))) ((s₁ , s₂) , s₃) + ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong [X⊗Y]⊗Z.fₛ (⟦⊕⟧-assocʳ i₁ i₂ i₃)) ⟩ + assocˡ ⟨$⟩ [X⊗Y]⊗Z.fₛ′ ((i₁ ⟦⊕⟧ i₂) ⟦⊕⟧ i₃) ((s₁ , s₂) , s₃) + ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) (cong (λg (< eval ∙ (X⊗Y.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Z.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ)) + (F.×-iso.isoʳ (A ⊕ B) C ((i₁ ⟦⊕⟧ i₂) , i₃))) ⟩ + assocˡ ⟨$⟩ (X⊗Y.fₛ′ (i₁ ⟦⊕⟧ i₂) (s₁ , s₂) , Z.fₛ′ i₃ s₃) + ≈⟨ cong (assocˡ {X.S} {Y.S} {Z.S}) + ((cong (λg (< eval ∙ (X.fₛ ∙ proj₁ₛ) ×-function proj₁ₛ , eval ∙ (Y.fₛ ∙ proj₂ₛ) ×-function proj₂ₛ >ₛ)) + (F.×-iso.isoʳ A B (i₁ , i₂))) , Z.S.refl) ⟩ + X.fₛ′ i₁ s₁ , (Y.fₛ′ i₂ s₂ , Z.fₛ′ i₃ s₃) + ∎ + where + open Setoids-CC using (λg; eval) + open ≈-Reasoning X⊗[Y⊗Z].S + open Func using (cong) + i₁ : Carrier (F.₀ A) + i₁ = proj₁ (⟦ F.×-iso.from A (B ⊕ C) ⟧ i) + i₂₃ : Carrier (F.₀ (B ⊕ C)) + i₂₃ = proj₂ (⟦ F.×-iso.from A (B ⊕ C) ⟧ i) + i₂ : Carrier (F.₀ B) + i₂ = proj₁ (⟦ F.×-iso.from B C ⟧ i₂₃) + i₃ : Carrier (F.₀ C) + i₃ = proj₂ (⟦ F.×-iso.from B C ⟧ i₂₃) + module A⊗B⊗C = CommutativeMonoid (F.₀ (A′ ⊕ (B′ ⊕ C′))) + ≗-fₒ + : fₒ′ (wire (S.assocʳ ∘ S.π₂) S.assocˡ (×-System (×-System X Y) Z)) ((s₁ , s₂) , s₃) + A⊗B⊗C.≈ fₒ′ (×-System X (×-System Y Z)) (s₁ , (s₂ , s₃)) + ≗-fₒ = begin + ⟦ F.₁ S.assocˡ ⟧ ((X.fₒ′ s₁ ⟦⊕⟧ Y.fₒ′ s₂) ⟦⊕⟧ Z.fₒ′ s₃) ≈⟨ ⟦⊕⟧-assocˡ (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃) ⟩ + X.fₒ′ s₁ ⟦⊕⟧ (Y.fₒ′ s₂ ⟦⊕⟧ Z.fₒ′ s₃) ∎ + where + open ≈-Reasoning A⊗B⊗C.setoid + +associativity + : {A B C : Box} + → Wire (S.assocʳ ∘ S.π₂) S.assocˡ ∘F η (A ⊞ B) C ∘F (η A B ∘F πˡ ※ IdF ∘F πʳ) + ≃ η A (B ⊞ C) ∘F (IdF ∘F πˡ ※ η B C ∘F πʳ) ∘F (πˡ ∘F πˡ ※ πʳ ∘F πˡ ※ πʳ) +associativity = + pointwise-iso + (λ { ((X , Y) , Z) → mk-≅ (≅.sym _ ×-assoc) (λ { i s → ≗-fₛ X Y Z s i }) λ { s → ≗-fₒ X Y Z s } }) + (λ { {(X , Y) , Z} {(X′ , Y′) , Z′} ((h , i) , j) → S.refl X′ , S.refl Y′ , S.refl Z′ }) + where + open Associativity + open System using (S) + +module Unitary {A B : Obj} (X : System (setoid (F.₀ A)) (F.₀ B)) where + + module X = System X + module ⊤⊗X = System (×-System (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)) X) + module X⊗⊤ = System (×-System X (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘))) + open System + + module B = CommutativeMonoid (F.₀ B) + + unitorˡ-≗fₛ + : (i : Carrier (F.₀ A)) + (s : ∣ X.S ∣) + → proj₂ (System.fₛ′ (wire (S.i₂ ∘ S.π₂) (S.π₂ {S.𝟘} {B}) (×-System (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)) X)) i (tt , s)) + X.S.≈ X.fₛ′ i s + unitorˡ-≗fₛ i s = begin + X.fₛ′ (⟦ F.₁ S.π₂ ⟧ (⟦ F.₁ (S.i₂ ∘ S.π₂) ⟧ (⊤⊗X.fₒ′ (tt , s) ⟦⊕⟧ i))) s ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₂) (F.homomorphism (⊤⊗X.fₒ′ (tt , s) ⟦⊕⟧ i))) ⟩ + X.fₛ′ (⟦ F.₁ S.π₂ ⟧ (⟦ F.₁ S.i₂ ⟧ (⟦ F.₁ S.π₂ ⟧ (⊤⊗X.fₒ′ (tt , s) ⟦⊕⟧ i)))) s ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₂) (⟦⟧-cong (F.₁ S.i₂) (F.F-resp-×.project₂ ((⊤⊗X.fₒ′ (tt , s) , i))))) ⟩ + X.fₛ′ (⟦ F.₁ S.π₂ ⟧ (⟦ F.₁ S.i₂ ⟧ i)) s ≈⟨ cong X.fₛ (F.homomorphism i) ⟨ + X.fₛ′ (⟦ F.₁ (S.π₂ ∘ S.i₂) ⟧ i) s ≈⟨ cong X.fₛ (F.F-resp-≈ S.π₂∘i₂≈id i) ⟩ + X.fₛ′ (⟦ F.₁ _ ⟧ i) s ≈⟨ cong X.fₛ (F.identity i) ⟩ + X.fₛ′ i s ∎ + where + open ≈-Reasoning X.S + open Func using (cong) + + unitorˡ-≗fₒ + : (s : ∣ X.S ∣) + → fₒ′ (wire (S.i₂ ∘ S.π₂) S.π₂ (×-System (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)) X)) (tt , s) B.≈ X.fₒ′ s + unitorˡ-≗fₒ s = begin + ⟦ F.₁ S.π₂ ⟧ (_ ⟦⊕⟧ X.fₒ′ s) ≈⟨ F.F-resp-×.project₂ (CommutativeMonoid.ε (F.₀ S.𝟘) , X.fₒ′ s) ⟩ + X.fₒ′ s ∎ + where + open ≈-Reasoning B.setoid + + unitorʳ-≗fₛ + : (i : Carrier (F.₀ A)) + (s : ∣ X.S ∣) + → proj₁ (System.fₛ′ (wire (S.i₁ ∘ S.π₂) (S.π₁ {B} {S.𝟘}) (×-System X (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)))) i (s , tt)) + X.S.≈ X.fₛ′ i s + unitorʳ-≗fₛ i s = begin + X.fₛ′ (⟦ F.₁ S.π₁ ⟧ (⟦ F.₁ (S.i₁ ∘ S.π₂) ⟧ (X⊗⊤.fₒ′ (s , tt) ⟦⊕⟧ i))) s ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₁) (F.homomorphism (X⊗⊤.fₒ′ (s , tt) ⟦⊕⟧ i))) ⟩ + X.fₛ′ (⟦ F.₁ _ ⟧ (⟦ F.₁ _ ⟧ (⟦ F.₁ S.π₂ ⟧ (_ ⟦⊕⟧ i)))) s ≈⟨ cong X.fₛ (⟦⟧-cong (F.₁ S.π₁) (⟦⟧-cong (F.₁ S.i₁) (F.F-resp-×.project₂ (_ , i)))) ⟩ + X.fₛ′ (⟦ F.₁ S.π₁ ⟧ (⟦ F.₁ S.i₁ ⟧ i)) s ≈⟨ cong X.fₛ (F.homomorphism i) ⟨ + X.fₛ′ (⟦ F.₁ (S.π₁ ∘ S.i₁) ⟧ i) s ≈⟨ cong X.fₛ (F.F-resp-≈ S.π₁∘i₁≈id i) ⟩ + X.fₛ′ (⟦ F.₁ _ ⟧ i) s ≈⟨ cong X.fₛ (F.identity i) ⟩ + X.fₛ′ i s ∎ + where + open ≈-Reasoning X.S + open Func using (cong) + + unitorʳ-≗fₒ + : (s : ∣ X.S ∣) + → fₒ′ (wire (S.i₁ ∘ S.π₂) S.π₁ (×-System X (discrete (setoid (F.₀ S.𝟘)) (F.₀ S.𝟘)))) (s , tt) B.≈ X.fₒ′ s + unitorʳ-≗fₒ s = begin + ⟦ F.₁ S.π₁ ⟧ (X.fₒ′ s ⟦⊕⟧ _) ≈⟨ F.F-resp-×.project₁ (X.fₒ′ s , CommutativeMonoid.ε (F.₀ S.𝟘)) ⟩ + X.fₒ′ s ∎ + where + open ≈-Reasoning B.setoid + +unitaryˡ + : {X : Box} + → Wire (S.i₂ ∘ S.π₂) S.π₂ ∘F η (S.𝟘 □ S.𝟘) X ∘F (ε ∘F πˡ ※ IdF ∘F πʳ) ≃ πʳ +unitaryˡ = + pointwise-iso + (λ (_ , X) → + mk-≅ + ⊤×A≅A + (λ i (_ , s) → unitorˡ-≗fₛ X i s) + (λ (_ , s) → unitorˡ-≗fₒ X s)) + λ { {_} {_ , B} _ → S.refl B } + where + open Unitary + open CartesianMonoidal Setoids-CC.cartesian using (⊤×A≅A) + open System using (module S) + +unitaryʳ + : {X : Box} + → Wire (S.i₁ ∘ S.π₂) S.π₁ ∘F η X (S.𝟘 □ S.𝟘) ∘F (IdF ∘F πˡ ※ ε ∘F πʳ) ≃ πˡ +unitaryʳ = + pointwise-iso + (λ (X , _) → + mk-≅ + A×⊤≅A + (λ i (s , _) → unitorʳ-≗fₛ X i s) + (λ (s , _) → unitorʳ-≗fₒ X s)) + λ { {_} {B , _} _ → S.refl B } + where + open Unitary + open CartesianMonoidal Setoids-CC.cartesian using (A×⊤≅A) + open System using (module S) + +Sys-IsMF : IsMonoidalFunctor DWD-MC Cats-MC Sys +Sys-IsMF = record + { ε = ε + ; ⊗-homo = ⊗-homo + ; associativity = associativity + ; unitaryˡ = unitaryˡ + ; unitaryʳ = unitaryʳ + } + +Sys-MF : MonoidalFunctor DWD-MC Cats-MC +Sys-MF = record + { F = Sys + ; isMonoidal = Sys-IsMF + } -- cgit v1.2.3