diff options
Diffstat (limited to 'Functor/Instance')
| -rw-r--r-- | Functor/Instance/WiringDiagram/System.agda | 70 |
1 files changed, 63 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 |