Generalize systems to (co)commutative (co)monoids

1 files changed, 48 insertions, 48 deletions

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