diff options
Diffstat (limited to 'Functor')
| -rw-r--r-- | Functor/Instance/WiringDiagram/System.agda | 70 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/WiringDiagram/System.agda | 422 |
2 files changed, 485 insertions, 7 deletions
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 + } |