From 7875edd03cce586a8c9f0b95dedffb390bfdbd61 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 9 Jul 2026 13:36:32 -0700 Subject: Generalize systems to (co)commutative (co)monoids --- Functor/Instance/Nat/System.agda | 96 ++++++++++++++++++++-------------------- 1 file changed, 48 insertions(+), 48 deletions(-) (limited to 'Functor/Instance/Nat/System.agda') diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda index 34ae65a..b9b89e4 100644 --- a/Functor/Instance/Nat/System.agda +++ b/Functor/Instance/Nat/System.agda @@ -6,7 +6,7 @@ module Functor.Instance.Nat.System where open import Level using (suc; 0ℓ) -import Data.System.Monoidal {suc 0ℓ} as System-⊗ +import Data.System.Monoidal as System-⊗ import Categories.Morphism as Morphism import Functor.Free.Instance.SymmetricMonoidalPreorder.Strong as SymmetricMonoidalPreorder @@ -26,7 +26,7 @@ open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-StrongSy open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper; NaturalIsomorphism) open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using () renaming (module Strong to Strong₂) open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Strong to Strong₄) -open import Category.Construction.CMonoids (Setoids-×.symmetric {suc 0ℓ} {suc 0ℓ}) using (CMonoids) +open import Category.Construction.CMonoids (Setoids-×.symmetric {suc 0ℓ} {0ℓ}) using (CMonoids) open import Category.Instance.SymMonCat using () renaming (module Strong to Strong₁) open import Data.Circuit.Value using (monoid) open import Data.Fin using (Fin) @@ -35,8 +35,8 @@ open import Data.Product using (_,_; _×_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Data.Setoid using (∣_∣) open import Data.Setoid.Unit using (⊤ₛ) -open import Data.System {suc 0ℓ} using (System; _≤_; _≈_; Systems[_,_]; ≤-refl; ≤-trans; discrete; Systems-MC; Systems-SMC) -open import Data.Values monoid using (module ≋; module Object; Values; ≋-isEquiv) +open import Data.System using (System; _≤_; _≈_; Systems[_,_]; ≤-refl; ≤-trans; discrete; Systems-MC; Systems-SMC) +open import Data.Values monoid using (module ≋; module Object; Values; ≋-isEquiv; module Algebra) open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id) open import Function.Construct.Identity using () renaming (function to Id) open import Function.Construct.Setoid using (_∙_) @@ -62,7 +62,7 @@ private opaque unfolding Valuesₘ ≋-isEquiv - map : (Fin A → Fin B) → System A A → System B B + map : (Fin A → Fin B) → System (Values A) (Algebra.Valuesₘ A) → System (Values B) (Algebra.Valuesₘ B) map {A} {B} f X = let open System X in record { S = S ; fₛ = fₛ ∙ arr (Pull.₁ f) @@ -72,7 +72,7 @@ opaque opaque unfolding map open System - map-≤ : (f : Fin A → Fin B) {X Y : System A A} → X ≤ Y → map f X ≤ map f Y + map-≤ : (f : Fin A → Fin B) {X Y : System (Values A) (Algebra.Valuesₘ A)} → X ≤ Y → map f X ≤ map f Y ⇒S (map-≤ f x≤y) = ⇒S x≤y ≗-fₛ (map-≤ f x≤y) = ≗-fₛ x≤y ∘ to (arr (Pull.₁ f)) ≗-fₒ (map-≤ f x≤y) = cong (arr (Push.₁ f)) ∘ ≗-fₒ x≤y @@ -81,15 +81,15 @@ opaque unfolding map-≤ map-≤-refl : (f : Fin A → Fin B) - → {X : System A A} - → map-≤ f (≤-refl {A} {A} {X}) ≈ ≤-refl + → {X : System (Values A) (Algebra.Valuesₘ A)} + → map-≤ f (≤-refl {x = X}) ≈ ≤-refl map-≤-refl f {X} = Setoid.refl (S (map f X)) opaque unfolding map-≤ map-≤-trans : (f : Fin A → Fin B) - → {X Y Z : System A A} + → {X Y Z : System (Values A) (Algebra.Valuesₘ A)} → {h : X ≤ Y} → {g : Y ≤ Z} → map-≤ f (≤-trans h g) ≈ ≤-trans (map-≤ f h) (map-≤ f g) @@ -99,13 +99,13 @@ opaque unfolding map-≤ map-≈ : (f : Fin A → Fin B) - → {X Y : System A A} + → {X Y : System (Values A) (Algebra.Valuesₘ A)} → {g h : X ≤ Y} → h ≈ g → map-≤ f h ≈ map-≤ f g map-≈ f h≈g = h≈g -Sys₁ : (Fin A → Fin B) → Functor Systems[ A , A ] Systems[ B , B ] +Sys₁ : (Fin A → Fin B) → Functor Systems[ Values A , Algebra.Valuesₘ A ] Systems[ Values B , Algebra.Valuesₘ B ] Sys₁ {A} {B} f = record { F₀ = map f ; F₁ = λ C≤D → map-≤ f C≤D @@ -116,14 +116,14 @@ Sys₁ {A} {B} f = record opaque unfolding map - map-id-≤ : (X : System A A) → map id X ≤ X + map-id-≤ : (X : System (Values A) (Algebra.Valuesₘ A)) → map id X ≤ X map-id-≤ X .⇒S = Id (S X) map-id-≤ X .≗-fₛ i s = cong (fₛ X) Pull.identity map-id-≤ X .≗-fₒ s = Push.identity opaque unfolding map - map-id-≥ : (X : System A A) → X ≤ map id X + map-id-≥ : (X : System (Values A) (Algebra.Valuesₘ A)) → X ≤ map id X map-id-≥ X .⇒S = Id (S X) map-id-≥ X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.identity) map-id-≥ X .≗-fₒ s = ≋.sym Push.identity @@ -131,7 +131,7 @@ opaque opaque unfolding map-≤ map-id-≤ map-id-comm - : {X Y : System A A} + : {X Y : System (Values A) (Algebra.Valuesₘ A)} (f : X ≤ Y) → ≤-trans (map-≤ id f) (map-id-≤ Y) ≈ ≤-trans (map-id-≤ X) f map-id-comm {Y} f = Setoid.refl (S Y) @@ -141,12 +141,12 @@ opaque unfolding map-id-≤ map-id-≥ map-id-isoˡ - : (X : System A A) + : (X : System (Values A) (Algebra.Valuesₘ A)) → ≤-trans (map-id-≤ X) (map-id-≥ X) ≈ ≤-refl map-id-isoˡ X = Setoid.refl (S X) map-id-isoʳ - : (X : System A A) + : (X : System (Values A) (Algebra.Valuesₘ A)) → ≤-trans (map-id-≥ X) (map-id-≤ X) ≈ ≤-refl map-id-isoʳ X = Setoid.refl (S X) @@ -166,7 +166,7 @@ opaque map-∘-≤ : (f : Fin A → Fin B) (g : Fin B → Fin C) - (X : System A A) + (X : System (Values A) (Algebra.Valuesₘ A)) → map (g ∘ f) X ≤ map g (map f X) map-∘-≤ f g X .⇒S = Id (S X) map-∘-≤ f g X .≗-fₛ i s = cong (fₛ X) Pull.homomorphism @@ -177,7 +177,7 @@ opaque map-∘-≥ : (f : Fin A → Fin B) (g : Fin B → Fin C) - (X : System A A) + (X : System (Values A) (Algebra.Valuesₘ A)) → map g (map f X) ≤ map (g ∘ f) X map-∘-≥ f g X .⇒S = Id (S X) map-∘-≥ f g X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.homomorphism) @@ -202,12 +202,12 @@ Sys-homo {A} f g = niHelper record map-∘-comm : (f : Fin A → Fin B) (g : Fin B → Fin C) - → {X Y : System A A} + → {X Y : System (Values A) (Algebra.Valuesₘ A)} (X≤Y : X ≤ Y) → ≤-trans (map-≤ (g ∘ f) X≤Y) (map-∘-≤ f g Y) ≈ ≤-trans (map-∘-≤ f g X) (map-≤ g (map-≤ f X≤Y)) map-∘-comm f g {Y} X≤Y = Setoid.refl (S Y) - module _ (X : System A A) where + module _ (X : System (Values A) (Algebra.Valuesₘ A)) where opaque unfolding map-∘-≤ map-∘-≥ isoˡ : ≤-trans (map-∘-≤ f g X) (map-∘-≥ f g X) ≈ ≤-refl @@ -215,7 +215,7 @@ Sys-homo {A} f g = niHelper record isoʳ : ≤-trans (map-∘-≥ f g X) (map-∘-≤ f g X) ≈ ≤-refl isoʳ = Setoid.refl (S X) -module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System A A) where +module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System (Values A) (Algebra.Valuesₘ A)) where opaque @@ -236,7 +236,7 @@ opaque map-cong-comm : {f g : Fin A → Fin B} (f≗g : f ≗ g) - {X Y : System A A} + {X Y : System (Values A) (Algebra.Valuesₘ A)} (h : X ≤ Y) → ≤-trans (map-≤ f h) (map-cong-≤ f≗g Y) ≈ ≤-trans (map-cong-≤ f≗g X) (map-≤ g h) @@ -249,14 +249,14 @@ opaque map-cong-isoˡ : {f g : Fin A → Fin B} (f≗g : f ≗ g) - (X : System A A) + (X : System (Values A) (Algebra.Valuesₘ A)) → ≤-trans (map-cong-≤ f≗g X) (map-cong-≥ f≗g X) ≈ ≤-refl map-cong-isoˡ f≗g X = Setoid.refl (S X) map-cong-isoʳ : {f g : Fin A → Fin B} (f≗g : f ≗ g) - (X : System A A) + (X : System (Values A) (Algebra.Valuesₘ A)) → ≤-trans (map-cong-≥ f≗g X) (map-cong-≤ f≗g X) ≈ ≤-refl map-cong-isoʳ f≗g X = Setoid.refl (S X) @@ -273,8 +273,8 @@ Sys-resp-≈ f≗g = niHelper record module NatCat where - Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ) - Sys .F₀ n = Systems[ n , n ] + Sys : Functor Nat (Cats (suc 0ℓ) 0ℓ 0ℓ) + Sys .F₀ n = Systems[ Values n , Algebra.Valuesₘ n ] Sys .F₁ = Sys₁ Sys .identity = Sys-identity Sys .homomorphism = Sys-homo _ _ @@ -286,15 +286,15 @@ module NatMC where module _ (f : Fin A → Fin B) where - module A = System-⊗ A A - module B = System-⊗ B B + module A = System-⊗ (Values A) (Algebra.Valuesₘ A) + module B = System-⊗ (Values B) (Algebra.Valuesₘ B) open CommutativeMonoid⇒ (Push.₁ f) - open Morphism Systems[ B , B ] using (_≅_) + open Morphism Systems[ Values B , Algebra.Valuesₘ B ] using (_≅_) opaque unfolding map - ε-≅ : discrete B B ≅ map f (discrete A A) + ε-≅ : discrete (Values B) (Algebra.Valuesₘ B) ≅ map f (discrete (Values A) (Algebra.Valuesₘ A)) ε-≅ = record -- other fields can be inferred { from = record @@ -335,7 +335,7 @@ module NatMC where module A-MC = MonoidalCategory A.Systems-MC module B-MC = MonoidalCategory B.Systems-MC - F : Functor Systems[ A , A ] Systems[ B , B ] + F : Functor Systems[ Values A , Algebra.Valuesₘ A ] Systems[ Values B , Algebra.Valuesₘ B ] F = Sys₁ f module F = Functor F @@ -347,7 +347,7 @@ module NatMC where unfolding ⊗-homo-≃ associativity - : {X Y Z : System A A} + : {X Y Z : System (Values A) (Algebra.Valuesₘ A)} → F.₁ A.Associator.assoc-≤ ∘′ ⊗-homo-≃.⇒.η (X A.⊗₀ Y , Z) ∘′ ⊗-homo-≃.⇒.η (X , Y) B.⊗₁ B-MC.id @@ -357,7 +357,7 @@ module NatMC where associativity {X} {Y} {Z} = Setoid.refl (S X ×ₛ (S Y ×ₛ S Z)) unitaryˡ - : {X : System A A} + : {X : System (Values A) (Algebra.Valuesₘ A)} → F.₁ A.Unitors.⊗-discreteˡ-≤ ∘′ ⊗-homo-≃.⇒.η (A-MC.unit , X) ∘′ ε-≅.from B.⊗₁ B-MC.id  @@ -365,14 +365,14 @@ module NatMC where unitaryˡ {X} = Setoid.refl (S X) unitaryʳ - : {X : System A A} + : {X : System (Values A) (Algebra.Valuesₘ A)} → F.₁ A.Unitors.⊗-discreteʳ-≤ - ∘′ ⊗-homo-≃.⇒.η (X , discrete A A) + ∘′ ⊗-homo-≃.⇒.η (X , discrete (Values A) (Algebra.Valuesₘ A)) ∘′ B-MC.id B.⊗₁ ε-≅.from B-MC.≈ B-MC.unitorʳ.from unitaryʳ {X} = Setoid.refl (S X) - Sys-MC₁ : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B) + Sys-MC₁ : StrongMonoidalFunctor (Systems-MC (Values A) (Algebra.Valuesₘ A)) (Systems-MC (Values B) (Algebra.Valuesₘ B)) Sys-MC₁ = record { F = Sys₁ f ; isStrongMonoidal = record @@ -386,7 +386,7 @@ module NatMC where opaque unfolding map-id-≤ ⊗-homo-≃ - Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC A A)) + Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC (Values A) (Algebra.Valuesₘ A))) Sys-MC-identity = record { U = NatCat.Sys.identity ; F⇒G-isMonoidal = record @@ -423,8 +423,8 @@ module NatMC where } } - Sys : Functor Nat (StrongMonoidals (suc 0ℓ) (suc 0ℓ) 0ℓ) - Sys .F₀ n = Systems-MC n n + Sys : Functor Nat (StrongMonoidals (suc 0ℓ) 0ℓ 0ℓ) + Sys .F₀ n = Systems-MC (Values n) (Algebra.Valuesₘ n) Sys .F₁ = Sys-MC₁ Sys .identity = Sys-MC-identity Sys .homomorphism = Sys-MC-homomorphism @@ -438,29 +438,29 @@ module NatSMC where private - module A = System-⊗ A A - module B = System-⊗ B B + module A = System-⊗ (Values A) (Algebra.Valuesₘ A) + module B = System-⊗ (Values B) (Algebra.Valuesₘ B) module A-SMC = SymmetricMonoidalCategory A.Systems-SMC module B-SMC = SymmetricMonoidalCategory B.Systems-SMC - F : Functor Systems[ A , A ] Systems[ B , B ] + F : Functor Systems[ Values A , Algebra.Valuesₘ A ] Systems[ Values B , Algebra.Valuesₘ B ] F = Sys₁ f module F = Functor F - F-MF : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B) + F-MF : StrongMonoidalFunctor (Systems-MC (Values A) (Algebra.Valuesₘ A)) (Systems-MC (Values B) (Algebra.Valuesₘ B)) F-MF = NatMC.Sys.₁ f module F-MF = StrongMonoidalFunctor F-MF opaque unfolding NatMC.⊗-homo-≃ σ-compat - : {X Y : System A A} + : {X Y : System (Values A) (Algebra.Valuesₘ A)} → F.₁ (A-SMC.braiding.⇒.η (X , Y)) B-SMC.∘ F-MF.⊗-homo.⇒.η (X , Y) B-SMC.≈ F-MF.⊗-homo.⇒.η (Y , X) B-SMC.∘ B-SMC.braiding.⇒.η (F.₀ X , F.₀ Y) σ-compat {X} {Y} = Setoid.refl (S Y ×ₛ S X) - Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC A A) (Systems-SMC B B) + Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC (Values A) (Algebra.Valuesₘ A)) (Systems-SMC (Values B) (Algebra.Valuesₘ B)) Sys-SMC₁ = record { F-MF ; isBraidedMonoidal = record @@ -469,7 +469,7 @@ module NatSMC where } } - Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC A A)) + Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC (Values A) (Algebra.Valuesₘ A))) Sys-SMC-identity = record { MonoidalNaturalIsomorphism NatMC.Sys.identity } Sys-SMC-homomorphism @@ -484,8 +484,8 @@ module NatSMC where → SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ f) (Sys-SMC₁ g) Sys-SMC-resp-≈ f≗g = record { MonoidalNaturalIsomorphism (NatMC.Sys.F-resp-≈ f≗g) } - Sys : Functor Nat (SymMonCat {suc 0ℓ} {suc 0ℓ} {0ℓ}) - Sys .F₀ n = Systems-SMC n n + Sys : Functor Nat SymMonCat + Sys .F₀ n = Systems-SMC (Values n) (Algebra.Valuesₘ n) Sys .F₁ = Sys-SMC₁ Sys .identity = Sys-SMC-identity Sys .homomorphism = Sys-SMC-homomorphism -- cgit v1.2.3