Generalize systems to (co)commutative (co)monoids

7 files changed, 463 insertions, 185 deletions

diff --git a/Data/System/Category.agda b/Data/System/Category.agda
index 171a003..50d950b 100644
--- a/Data/System/Category.agda
+++ b/Data/System/Category.agda
@@ -1,15 +1,15 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ; suc)
+open import Level using (Level; suc; _⊔_)
 
-module Data.System.Category {ℓ : Level} where
+module Data.System.Category {c ℓ : Level} where
 
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
+open import Algebra using (CommutativeMonoid)
 open import Categories.Category using (Category)
-open import Data.Nat using (ℕ)
-open import Data.System.Core {ℓ} using (System; _≤_; ≤-trans; ≤-refl)
 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)
 
@@ -17,13 +17,13 @@ open Func
 open System
 open _≤_
 
-private module ≈ {n m : ℕ} where
+private module ≈ {I : Setoid c ℓ} {O : CommutativeMonoid c ℓ} where
 
   private
     variable
-      A B C : System n m
+      A B C : System I O
 
-  _≈_ : Rel (A ≤ B) 0ℓ
+  _≈_ : Rel (A ≤ B) ℓ
   _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
     where
       module A⇒B = Setoid (S A ⇒ₛ S B)
@@ -46,9 +46,9 @@ private module ≈ {n m : ℕ} where
 open ≈ using (_≈_) public
 open ≈ using (≈-isEquiv; ≤-resp-≈)
 
-Systems[_,_] : ℕ → ℕ → Category (suc 0ℓ) ℓ 0ℓ
-Systems[ n , m ] = record
-    { Obj = System n m
+Systems[_,_] : Setoid c ℓ → CommutativeMonoid c ℓ → Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
+Systems[ I , O ] = record
+    { Obj = System I O
     ; _⇒_ = _≤_
     ; _≈_ = _≈_
     ; id = ≤-refl
diff --git a/Data/System/Core.agda b/Data/System/Core.agda
index 3616847..d64045a 100644
--- a/Data/System/Core.agda
+++ b/Data/System/Core.agda
@@ -1,16 +1,14 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ; suc)
+open import Level using (Level; 0ℓ; suc; _⊔_)
 
-module Data.System.Core {ℓ : Level} where
+module Data.System.Core {c ℓ : Level} where
 
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-open import Data.Circuit.Value using (monoid)
-open import Data.Nat using (ℕ)
+open import Algebra using (CommutativeMonoid)
 open import Data.Setoid using (_⇒ₛ_; ∣_∣)
 open import Data.Setoid.Unit using (⊤ₛ)
-open import Data.Values monoid using (Values; _≋_; module ≋; <ε>)
 open import Function using (Func; _⟨$⟩_)
 open import Function.Construct.Constant using () renaming (function to Const)
 open import Function.Construct.Identity using () renaming (function to Id)
@@ -22,34 +20,49 @@ open Func
 -- A dynamical system with a set of states,
 -- a state update function,
 -- and a readout function
-record System (n m : ℕ) : Set₁ where
+
+-- Really, the input type should be a cocommutative comonoid,
+-- but every setoid is a cocommutative comonoid in a unique way
+record System (I : Setoid c ℓ) (O : CommutativeMonoid c ℓ) : Set (c ⊔ suc ℓ) where
+
+  private
+    module I = Setoid I
+    module O = CommutativeMonoid O
 
   field
-    S : Setoid 0ℓ 0ℓ
-    fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
-    fₒ : ∣ S ⇒ₛ Values m ∣
+    S : Setoid ℓ ℓ
+    fₛ : ∣ I ⇒ₛ S ⇒ₛ S ∣
+    fₒ : ∣ S ⇒ₛ O.setoid ∣
 
-  fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
+  fₛ′ : I.Carrier → ∣ S ∣ → ∣ S ∣
   fₛ′ i = to (to fₛ i)
 
-  fₒ′ : ∣ S ∣ → ∣ Values m ∣
+  fₒ′ : ∣ S ∣ → O.Carrier
   fₒ′ = to fₒ
 
   module S = Setoid S
 
 open System
 
--- the discrete system from n nodes to m nodes
-discrete : (n m : ℕ) → System n m
-discrete _ _ .S = ⊤ₛ
-discrete n _ .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ)
-discrete _ m .fₒ = Const ⊤ₛ (Values m) <ε>
+module _ where
+
+  open CommutativeMonoid
+
+  -- the discrete system ignores input and outputs default value
+  discrete : (I : Setoid c ℓ) (O : CommutativeMonoid c ℓ) → System I O
+  discrete _ _ .S = ⊤ₛ
+  discrete I _ .fₛ = Const I (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ)
+  discrete _ O .fₒ = Const ⊤ₛ (setoid O) (ε O)
+
+module _ {I : Setoid c ℓ} {O : CommutativeMonoid c ℓ} where
 
-module _ {n m : ℕ} where
+  private
+    module I = Setoid I
+    module O = CommutativeMonoid O
 
   -- Simulation of systems: a mapping of internal
   -- states which respects i/o behavior
-  record _≤_ (A B : System n m) : Set ℓ where
+  record _≤_ (A B : System I O) : Set (c ⊔ ℓ) where
 
     private
       module A = System A
@@ -57,8 +70,8 @@ module _ {n m : ℕ} where
 
     field
       ⇒S : ∣ A.S ⇒ₛ B.S ∣
-      ≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
-      ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s)
+      ≗-fₛ : (i : I.Carrier) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
+      ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s O.≈ B.fₒ′ (⇒S ⟨$⟩ s)
 
   infix 4 _≤_
 
@@ -69,7 +82,7 @@ module _ {n m : ℕ} where
   ≤-refl : Reflexive _≤_
   ⇒S ≤-refl = Id _
   ≗-fₛ (≤-refl {x}) _ _ = S.refl x
-  ≗-fₒ ≤-refl _ = ≋.refl
+  ≗-fₒ ≤-refl _ = O.refl
 
   -- ≤ is transitive: if B simulates A, and C simulates B, then C simulates A
   ≤-trans : Transitive _≤_
@@ -78,7 +91,7 @@ module _ {n m : ℕ} where
       ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩
       ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩
       fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
-  ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values m) in begin
+  ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning O.setoid in begin
       fₒ′ x s                       ≈⟨ ≗-fₒ a s ⟩
       fₒ′ y (⇒S a ⟨$⟩ s)            ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩
       fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
diff --git a/Data/System/Looped.agda b/Data/System/Looped.agda
index 96f3432..1fd86d6 100644
--- a/Data/System/Looped.agda
+++ b/Data/System/Looped.agda
@@ -1,74 +1,79 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ; suc)
+open import Level using (Level; suc; _⊔_)
 
-module Data.System.Looped {ℓ : Level} where
+module Data.System.Looped {c ℓ : Level} where
 
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
+open import Algebra using (CommutativeMonoid)
 open import Categories.Category using (Category)
 open import Categories.Category.Helper using (categoryHelper)
 open import Categories.Functor using (Functor)
-open import Data.Nat using (ℕ)
-open import Data.System.Category {ℓ} using (Systems[_,_])
-open import Data.System.Core {ℓ} using (System; _≤_)
-open import Categories.Functor using (Functor)
-open import Data.Circuit.Value using (monoid)
-open import Data.Values monoid using (_⊕_; ⊕-cong; module ≋)
-open import Relation.Binary using (Setoid)
+open import Data.System.Category using (Systems[_,_])
+open import Data.System.Core using (System; _≤_)
 open import Function using (Func; _⟨$⟩_) renaming (id to idf)
+open import Relation.Binary using (Setoid)
 
 open Func
 open System
 
 private
 
-  loop : {n : ℕ} → System n n → System n n
-  loop X = record
-      { S = X.S
-      ; fₛ = record
-          { to = λ i → record
-              { to = λ s → X.fₛ′ (i ⊕ X.fₒ′ s) s
-              ; cong = λ {s} {s′} ≈s → X.S.trans
-                  (cong X.fₛ (⊕-cong ≋.refl (cong X.fₒ ≈s))) (cong (X.fₛ ⟨$⟩ (i ⊕ X.fₒ′ s′)) ≈s)
-              }
-          ; cong = λ ≋v → cong X.fₛ (⊕-cong ≋v ≋.refl)
-          }
-      ; fₒ = X.fₒ
-      }
-    where
-      module X = System X
+  module _ {V : CommutativeMonoid c ℓ} where
 
-  loop-≤ : {n : ℕ} {A B : System n n} → A ≤ B → loop A ≤ loop B
-  loop-≤ {_} {A} {B} A≤B = record
-      { ⇒S = A≤B.⇒S
-      ; ≗-fₛ = λ i s → begin
-          A≤B.⇒S ⟨$⟩ (fₛ′ (loop A) i s)                   ≈⟨ A≤B.≗-fₛ (i ⊕ A.fₒ′ s) s ⟩
-          B.fₛ′ (i ⊕ A.fₒ′ s) (A≤B.⇒S ⟨$⟩ s)              ≈⟨ cong B.fₛ (⊕-cong ≋.refl (A≤B.≗-fₒ s)) ⟩
-          B.fₛ′ (i ⊕ B.fₒ′ (A≤B.⇒S ⟨$⟩ s)) (A≤B.⇒S ⟨$⟩ s) ∎
-      ; ≗-fₒ = A≤B.≗-fₒ
-      }
-    where
-      module A = System A
-      module B = System B
-      open ≈-Reasoning B.S
-      module A≤B = _≤_ A≤B
+    open CommutativeMonoid V
 
-Loop : (n : ℕ) → Functor Systems[ n , n ] Systems[ n , n ]
-Loop n = record
-    { F₀ = loop
-    ; F₁ = loop-≤
-    ; identity = λ {A} → Setoid.refl (S A)
-    ; homomorphism = λ {Z = Z} → Setoid.refl (S Z)
-    ; F-resp-≈ = idf
-    }
+    loop : System setoid V → System setoid V
+    loop X = record
+        { S = X.S
+        ; fₛ = record
+            { to = λ i → record
+                { to = λ s → X.fₛ′ (i ∙ X.fₒ′ s) s
+                ; cong = λ {s} {s′} ≈s →
+                    X.S.trans
+                      (cong X.fₛ (∙-cong refl (cong X.fₒ ≈s)))
+                      (cong (X.fₛ ⟨$⟩ (i ∙ X.fₒ′ s′)) ≈s)
+                }
+            ; cong = λ ≈v → cong X.fₛ (∙-congʳ ≈v)
+            }
+        ; fₒ = X.fₒ
+        }
+      where
+        module X = System X
 
-module _ (n : ℕ) where
+    loop-≤ : {A B : System setoid V} → A ≤ B → loop A ≤ loop B
+    loop-≤ {A} {B} A≤B = record
+        { ⇒S = A≤B.⇒S
+        ; ≗-fₛ = λ i s → begin
+            A≤B.⇒S ⟨$⟩ (fₛ′ (loop A) i s)                   ≈⟨ A≤B.≗-fₛ (i ∙ A.fₒ′ s) s ⟩
+            B.fₛ′ (i ∙ A.fₒ′ s) (A≤B.⇒S ⟨$⟩ s)              ≈⟨ cong B.fₛ (∙-cong refl (A≤B.≗-fₒ s)) ⟩
+            B.fₛ′ (i ∙ B.fₒ′ (A≤B.⇒S ⟨$⟩ s)) (A≤B.⇒S ⟨$⟩ s) ∎
+        ; ≗-fₒ = A≤B.≗-fₒ
+        }
+      where
+        module A = System A
+        module B = System B
+        open ≈-Reasoning B.S
+        module A≤B = _≤_ A≤B
+
+module _ (V : CommutativeMonoid c ℓ) where
+
+  open CommutativeMonoid V using (setoid)
+
+  Loop : Functor Systems[ setoid , V ] Systems[ setoid , V ]
+  Loop = record
+      { F₀ = loop
+      ; F₁ = loop-≤
+      ; identity = λ {A} → Setoid.refl (S A)
+      ; homomorphism = λ {Z = Z} → Setoid.refl (S Z)
+      ; F-resp-≈ = idf
+      }
 
-  open Category Systems[ n , n ]
-  open Functor (Loop n)
+  open Category Systems[ setoid , V ]
+  open Functor Loop
 
-  Systems[_] : Category (suc 0ℓ) ℓ 0ℓ
+  Systems[_] : Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
   Systems[_] = categoryHelper record
       { Obj = Obj
       ; _⇒_ = _⇒_
diff --git a/Data/System/Looped/Monoidal.agda b/Data/System/Looped/Monoidal.agda
index af3d77c..81d5f7d 100644
--- a/Data/System/Looped/Monoidal.agda
+++ b/Data/System/Looped/Monoidal.agda
@@ -1,28 +1,30 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ; suc)
+open import Level using (Level; suc; _⊔_)
 
-module Data.System.Looped.Monoidal {ℓ : Level} where
+module Data.System.Looped.Monoidal {c ℓ : Level} where
 
 import Categories.Morphism as Morphism
-import Data.System.Monoidal {ℓ} as Unlooped
+import Data.System.Monoidal as Unlooped
 
+open import Algebra using (CommutativeMonoid)
 open import Categories.Category.Monoidal using (Monoidal)
 open import Categories.Category.Monoidal.Symmetric using (Symmetric)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
 open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
 open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor)
-open import Data.Nat using (ℕ)
-open import Data.System.Core {ℓ} using (System)
-open import Data.System.Looped {ℓ} using (Systems[_])
+open import Data.System.Core using (System)
+open import Data.System.Looped using (Systems[_])
 
-module _ (n : ℕ) where
+module _ (V : CommutativeMonoid c ℓ) where
 
   private
 
-    module Systems-MC = MonoidalCategory (Unlooped.Systems-MC n n)
+    module V = CommutativeMonoid V
 
-    ⊗ : Bifunctor Systems[ n ] Systems[ n ] Systems[ n ]
+    module Systems-MC = MonoidalCategory (Unlooped.Systems-MC V.setoid V)
+
+    ⊗ : Bifunctor Systems[ V ] Systems[ V ] Systems[ V ]
     ⊗ = record
         { F₀ = Systems-MC.⊗.₀
         ; F₁ = Systems-MC.⊗.₁
@@ -31,9 +33,9 @@ module _ (n : ℕ) where
         ; F-resp-≈ = λ {f = f} {g} → Systems-MC.⊗.F-resp-≈ {f = f} {g}
         }
 
-    module _ {X : System n n} where
+    module _ {X : System V.setoid V} where
 
-      open Morphism Systems[ n ] using (_≅_; module Iso)
+      open Morphism Systems[ V ] using (_≅_; module Iso)
       open Systems-MC using (_⊗₀_)
 
       unitorˡ : Systems-MC.unit ⊗₀ X ≅ X
@@ -56,13 +58,13 @@ module _ (n : ℕ) where
               }
           }
 
-    module _ {X Y Z : System n n} where
+    module _ {X Y Z : System V.setoid V} where
 
       module X = System X
       module Y = System Y
       module Z = System Z
 
-      open Morphism Systems[ n ] using (_≅_; module Iso)
+      open Morphism Systems[ V ] using (_≅_; module Iso)
       open Systems-MC using (_⊗₀_)
 
       associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)
@@ -75,7 +77,7 @@ module _ (n : ℕ) where
               }
           }
 
-  Systems-Monoidal : Monoidal Systems[ n ]
+  Systems-Monoidal : Monoidal Systems[ V ]
   Systems-Monoidal = record
       { ⊗ = ⊗
       ; unit = Systems-MC.unit
@@ -94,7 +96,7 @@ module _ (n : ℕ) where
 
   private
 
-    module Systems-SMC = SymmetricMonoidalCategory (Unlooped.Systems-SMC n n)
+    module Systems-SMC = SymmetricMonoidalCategory (Unlooped.Systems-SMC V.setoid V)
 
     braiding : ⊗ ≃ flip-bifunctor ⊗
     braiding = record
@@ -113,8 +115,8 @@ module _ (n : ℕ) where
       ; commutative = λ {X Y} → Systems-SMC.commutative {X} {Y}
       }
 
-  Systems-MC : MonoidalCategory (suc 0ℓ) ℓ 0ℓ
+  Systems-MC : MonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
   Systems-MC = record { monoidal = Systems-Monoidal }
 
-  Systems-SMC : SymmetricMonoidalCategory (suc 0ℓ) ℓ 0ℓ
+  Systems-SMC : SymmetricMonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
   Systems-SMC = record { symmetric = Systems-Symmetric }
diff --git a/Data/System/Monoidal.agda b/Data/System/Monoidal.agda
index cdf06e2..1c24e07 100644
--- a/Data/System/Monoidal.agda
+++ b/Data/System/Monoidal.agda
@@ -1,46 +1,48 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Data.Nat using (ℕ)
-open import Level using (Level; suc; 0ℓ)
+open import Algebra using (CommutativeMonoid)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary using (Setoid)
 
-module Data.System.Monoidal {ℓ : Level} (n m : ℕ) where
+module Data.System.Monoidal {c ℓ : Level} (I : Setoid c ℓ) (O : CommutativeMonoid c ℓ) where
 
-open import Data.System.Core {ℓ} using (System; _≤_; ≤-refl; ≤-trans; discrete)
-open import Data.System.Category {ℓ} using (Systems[_,_])
+open import Data.System.Core using (System; _≤_; ≤-refl; ≤-trans; discrete)
+open import Data.System.Category using (Systems[_,_])
 
 open import Categories.Category.Monoidal using (Monoidal)
-open import Categories.Category.Monoidal.Symmetric using (Symmetric)
 open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
 open import Categories.Functor using (Functor)
 open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor)
-open import Categories.Morphism (Systems[ n , m ]) using (_≅_; Iso)
+open import Categories.Morphism (Systems[ I , O ]) using (_≅_; Iso)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
-open import Data.Circuit.Value using (monoid)
 open import Data.Product using (_,_; _×_; uncurry′)
 open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; swapₛ)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Setoid using (_⇒ₛ_; _×-⇒_; assocₛ⇒; assocₛ⇐)
-open import Data.Values monoid using (Values; _⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ; ⊕-assoc; ⊕-comm; module ≋)
 open import Function using (Func; _⟶ₛ_)
 open import Function.Construct.Setoid using (_∙_)
-open import Relation.Binary using (Setoid)
 
 open _≤_
 open Setoid
 
+private
+  module I = Setoid I
+  module O = CommutativeMonoid O
+
 module _ where
 
   open Func
 
-  δₛ : Values n ⟶ₛ Values n ×ₛ Values n
+  δₛ : I ⟶ₛ I ×ₛ I
   δₛ .to v = v , v
   δₛ .cong v≋w = v≋w , v≋w
 
-  ⊕ₛ : Values m ×ₛ Values m ⟶ₛ Values m
-  ⊕ₛ .to (v , w) = v ⊕ w
-  ⊕ₛ .cong (v₁≋v₂ , w₁≋w₂) = ⊕-cong v₁≋v₂ w₁≋w₂
+  ⊕ₛ : O.setoid ×ₛ O.setoid ⟶ₛ O.setoid
+  ⊕ₛ .to (v , w) = v O.∙ w
+  ⊕ₛ .cong (v₁≈v₂ , w₁≈w₂) = O.∙-cong v₁≈v₂ w₁≈w₂
 
-_⊗₀_ : System n m → System n m → System n m
+_⊗₀_ : System I O → System I O → System I O
 _⊗₀_ X Y = let open System in record
     { S = S X ×ₛ S Y
     ; fₛ = fₛ X ×-⇒ fₛ Y ∙ δₛ
@@ -48,60 +50,60 @@ _⊗₀_ X Y = let open System in record
     }
 
 _⊗₁_
-    : {A A′ B B′ : System n m}
+    : {A A′ B B′ : System I O}
       (f : A ≤ A′)
       (g : B ≤ B′)
     → A ⊗₀ B ≤ A′ ⊗₀ B′
 _⊗₁_ f g .⇒S = ⇒S f ×-function ⇒S g
 _⊗₁_ f g .≗-fₛ i (s₁ , s₂) = ≗-fₛ f i s₁ , ≗-fₛ g i s₂
-_⊗₁_ f g .≗-fₒ (s₁ , s₂) = ⊕-cong (≗-fₒ f s₁) (≗-fₒ g s₂)
+_⊗₁_ f g .≗-fₒ (s₁ , s₂) = O.∙-cong (≗-fₒ f s₁) (≗-fₒ g s₂)
 
 module _ where
 
   open Functor
   open System
 
-  ⊗ : Bifunctor Systems[ n , m ] Systems[ n , m ] Systems[ n , m ]
+  ⊗ : Bifunctor Systems[ I , O ] Systems[ I , O ] Systems[ I , O ]
   ⊗ .F₀ = uncurry′ _⊗₀_
   ⊗ .F₁ = uncurry′ _⊗₁_
   ⊗ .identity {X , Y} = refl (S X) , refl (S Y)
   ⊗ .homomorphism {_} {_} {X″ , Y″} = refl (S X″) , refl (S Y″)
   ⊗ .F-resp-≈ (f≈f′ , g≈g′) = f≈f′ , g≈g′
 
-module Unitors {X : System n m} where
+module Unitors {X : System I O} where
 
   open System X
 
-  ⊗-discreteˡ-≤ : discrete n m ⊗₀ X ≤ X
+  ⊗-discreteˡ-≤ : discrete I O ⊗₀ X ≤ X
   ⊗-discreteˡ-≤ .⇒S = proj₂ₛ
   ⊗-discreteˡ-≤ .≗-fₛ i s = S.refl
-  ⊗-discreteˡ-≤ .≗-fₒ (_ , s) = ⊕-identityˡ (fₒ′ s)
+  ⊗-discreteˡ-≤ .≗-fₒ (_ , s) = O.identityˡ (fₒ′ s)
 
-  ⊗-discreteˡ-≥ : X ≤ discrete n m ⊗₀ X
+  ⊗-discreteˡ-≥ : X ≤ discrete I O ⊗₀ X
   ⊗-discreteˡ-≥ .⇒S = record { to = λ s → _ , s ; cong = λ s≈s′ → _ , s≈s′ }
   ⊗-discreteˡ-≥ .≗-fₛ i s = _ , S.refl
-  ⊗-discreteˡ-≥ .≗-fₒ s = ≋.sym (⊕-identityˡ (fₒ′ s))
+  ⊗-discreteˡ-≥ .≗-fₒ s = O.sym (O.identityˡ (fₒ′ s))
 
-  ⊗-discreteʳ-≤ : X ⊗₀ discrete n m ≤ X
+  ⊗-discreteʳ-≤ : X ⊗₀ discrete I O ≤ X
   ⊗-discreteʳ-≤ .⇒S = proj₁ₛ
   ⊗-discreteʳ-≤ .≗-fₛ i s = S.refl
-  ⊗-discreteʳ-≤ .≗-fₒ (s , _) = ⊕-identityʳ (fₒ′ s)
+  ⊗-discreteʳ-≤ .≗-fₒ (s , _) = O.identityʳ (fₒ′ s)
 
-  ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete n m
+  ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete I O
   ⊗-discreteʳ-≥ .⇒S = record { to = λ s → s , _ ; cong = λ s≈s′ → s≈s′ , _ }
   ⊗-discreteʳ-≥ .≗-fₛ i s = S.refl , _
-  ⊗-discreteʳ-≥ .≗-fₒ s = ≋.sym (⊕-identityʳ (fₒ′ s))
+  ⊗-discreteʳ-≥ .≗-fₒ s = O.sym (O.identityʳ (fₒ′ s))
 
   open _≅_
   open Iso
 
-  unitorˡ : discrete n m ⊗₀ X ≅ X
+  unitorˡ : discrete I O ⊗₀ X ≅ X
   unitorˡ .from = ⊗-discreteˡ-≤
   unitorˡ .to = ⊗-discreteˡ-≥
   unitorˡ .iso .isoˡ = _ , S.refl
   unitorˡ .iso .isoʳ = S.refl
 
-  unitorʳ : X ⊗₀ discrete n m ≅ X
+  unitorʳ : X ⊗₀ discrete I O ≅ X
   unitorʳ .from = ⊗-discreteʳ-≤
   unitorʳ .to = ⊗-discreteʳ-≥
   unitorʳ .iso .isoˡ = S.refl , _
@@ -109,7 +111,7 @@ module Unitors {X : System n m} where
 
 open Unitors using (unitorˡ; unitorʳ) public
 
-module Associator {X Y Z : System n m} where
+module Associator {X Y Z : System I O} where
 
   module X = System X
   module Y = System Y
@@ -118,12 +120,12 @@ module Associator {X Y Z : System n m} where
   assoc-≤ : (X ⊗₀ Y) ⊗₀ Z ≤ X ⊗₀ (Y ⊗₀ Z)
   assoc-≤ .⇒S = assocₛ⇒
   assoc-≤ .≗-fₛ i ((s₁ , s₂) , s₃) = X.S.refl , Y.S.refl , Z.S.refl
-  assoc-≤ .≗-fₒ ((s₁ , s₂) , s₃) = ⊕-assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃)
+  assoc-≤ .≗-fₒ ((s₁ , s₂) , s₃) = O.assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃)
 
   assoc-≥ : X ⊗₀ (Y ⊗₀ Z) ≤ (X ⊗₀ Y) ⊗₀ Z
   assoc-≥ .⇒S = assocₛ⇐
   assoc-≥ .≗-fₛ i (s₁ , (s₂ , s₃)) = (X.S.refl , Y.S.refl) , Z.S.refl
-  assoc-≥ .≗-fₒ (s₁ , (s₂ , s₃)) = ≋.sym (⊕-assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃) )
+  assoc-≥ .≗-fₒ (s₁ , (s₂ , s₃)) = O.sym (O.assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃) )
 
   open _≅_
   open Iso
@@ -136,10 +138,10 @@ module Associator {X Y Z : System n m} where
 
 open Associator using (associator) public
 
-Systems-Monoidal : Monoidal Systems[ n , m ]
+Systems-Monoidal : Monoidal Systems[ I , O ]
 Systems-Monoidal = let open System in record
     { ⊗ = ⊗
-    ; unit = discrete n m
+    ; unit = discrete I O
     ; unitorˡ = unitorˡ
     ; unitorʳ = unitorʳ
     ; associator = associator
@@ -155,10 +157,10 @@ Systems-Monoidal = let open System in record
 
 open System
 
-⊗-swap-≤ : {X Y : System n m} → Y ⊗₀ X ≤ X ⊗₀ Y
+⊗-swap-≤ : {X Y : System I O} → Y ⊗₀ X ≤ X ⊗₀ Y
 ⊗-swap-≤ .⇒S = swapₛ
 ⊗-swap-≤ {X} {Y} .≗-fₛ i (s₁ , s₂) = refl (S X) , refl (S Y)
-⊗-swap-≤ {X} {Y} .≗-fₒ (s₁ , s₂) = ⊕-comm (fₒ′ Y s₁) (fₒ′ X s₂)
+⊗-swap-≤ {X} {Y} .≗-fₒ (s₁ , s₂) = O.comm (fₒ′ Y s₁) (fₒ′ X s₂)
 
 braiding : ⊗ ≃ flip-bifunctor ⊗
 braiding = niHelper record
@@ -181,8 +183,8 @@ Systems-Symmetric = record
     ; commutative = λ {X} {Y} → refl (S Y) , refl (S X)
     }
 
-Systems-MC : MonoidalCategory (suc 0ℓ) ℓ 0ℓ
+Systems-MC : MonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
 Systems-MC = record { monoidal = Systems-Monoidal }
 
-Systems-SMC : SymmetricMonoidalCategory (suc 0ℓ) ℓ 0ℓ
+Systems-SMC : SymmetricMonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
 Systems-SMC = record { symmetric = Systems-Symmetric }
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
diff --git a/Functor/Instance/Nat/System/Looped.agda b/Functor/Instance/Nat/System/Looped.agda
new file mode 100644
index 0000000..86ebd81
--- /dev/null
+++ b/Functor/Instance/Nat/System/Looped.agda
@@ -0,0 +1,256 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
+{-# OPTIONS --lossy-unification #-}
+
+module Functor.Instance.Nat.System.Looped where
+
+open import Level using (suc; 0ℓ)
+
+import Data.System.Monoidal as System-⊗
+import Functor.Instance.Nat.System as Unlooped
+import Categories.Morphism as Morphism
+import Functor.Free.Instance.SymmetricMonoidalPreorder.Strong as SymmetricMonoidalPreorder
+
+open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
+
+open import Categories.Category.Instance.Cats using (Cats)
+open import Categories.Category.Instance.Monoidals using (StrongMonoidals)
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
+open import Categories.Functor.Monoidal.Properties using (idF-StrongMonoidal; ∘-StrongMonoidal)
+open import Categories.Functor.Monoidal.Symmetric using () renaming (module Strong to Strong₃)
+open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-StrongSymmetricMonoidal; ∘-StrongSymmetricMonoidal)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; 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ℓ} {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)
+open import Data.Nat using (ℕ)
+open import Data.System using (System; _≤_; _≈_; Systems[_]; ≤-refl; ≤-trans; discrete)
+open import Data.System.Looped.Monoidal using (Systems-MC; Systems-SMC)
+open import Data.Values monoid using (module ≋; module Algebra; Values; ≋-isEquiv)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
+open import Function.Construct.Setoid using (_∙_)
+open import Functor.Free.Instance.InducedCMonoid using (InducedCMonoid)
+open import Functor.Instance.Nat.Pull using (Pull)
+open import Functor.Instance.Nat.Push using (Push)
+open import Object.Monoid.Commutative (Setoids-×.symmetric {0ℓ} {0ℓ}) using (CommutativeMonoid; CommutativeMonoid⇒)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+
+open Functor
+open Strong₁ using (SymMonCat)
+open Strong₂ using (MonoidalNaturalIsomorphism)
+open Strong₃ using (SymmetricMonoidalFunctor)
+open Strong₄ using (SymmetricMonoidalNaturalIsomorphism)
+open Algebra using (Valuesₘ)
+
+private
+  variable A B C : ℕ
+
+opaque
+
+  unfolding ≋-isEquiv
+
+  Sys₁ : (Fin A → Fin B) → Functor Systems[ Valuesₘ A ] Systems[ Valuesₘ B ]
+  Sys₁ f = record { Functor (Unlooped.NatCat.Sys.₁ f) }
+
+  Sys-identity : Sys₁ {A} id ≃ idF
+  Sys-identity {A} = record
+      { F⇒G = record { NI.⇒ }
+      ; F⇐G = record { NI.⇐ }
+      ; iso = λ X → record { NI.iso X }
+      }
+    where
+      module NI = NaturalIsomorphism (Unlooped.NatCat.Sys.identity {A})
+
+  Sys-homo
+      : (f : Fin A → Fin B)
+        (g : Fin B → Fin C)
+      → Sys₁ (g ∘ f) ≃ Sys₁ g ∘F Sys₁ f
+  Sys-homo {A} f g = record
+      { F⇒G = record { NI.⇒ }
+      ; F⇐G = record { NI.⇐ }
+      ; iso = λ X → record { NI.iso X }
+      }
+    where
+      module NI = NaturalIsomorphism (Unlooped.NatCat.Sys.homomorphism {f = f} {g})
+
+  Sys-resp-≈ : {f g : Fin A → Fin B} → f ≗ g → Sys₁ f ≃ Sys₁ g
+  Sys-resp-≈ f≗g = record
+      { F⇒G = record { NI.⇒ }
+      ; F⇐G = record { NI.⇐ }
+      ; iso = λ X → record { NI.iso X }
+      }
+    where
+      module NI = NaturalIsomorphism (Unlooped.NatCat.Sys.F-resp-≈ f≗g)
+
+module NatCat where
+
+  Sys : Functor Nat (Cats (suc 0ℓ) 0ℓ 0ℓ)
+  Sys .F₀ = λ n → Systems[ Valuesₘ n ]
+  Sys .F₁ = Sys₁
+  Sys .identity = Sys-identity
+  Sys .homomorphism = Sys-homo _ _
+  Sys .F-resp-≈ = Sys-resp-≈
+
+  module Sys = Functor Sys
+
+module NatMC where
+
+  module _ (f : Fin A → Fin B) where
+
+    -- module A = System-⊗ A A
+    -- module B = System-⊗ B B
+
+    module MF = StrongMonoidalFunctor (Unlooped.NatMC.Sys.₁ f)
+
+    open Morphism using (_≅_; Iso)
+
+    opaque
+
+      unfolding Sys₁ ≋-isEquiv
+
+      Sys-MC₁ : StrongMonoidalFunctor (Systems-MC (Valuesₘ A)) (Systems-MC (Valuesₘ B))
+      Sys-MC₁ = record
+          { F = Sys₁ f
+          ; isStrongMonoidal = record
+              { ε = record
+                  { _≅_ MF.ε
+                  ; iso = record { Iso MF.ε.iso }
+                  }
+              ; ⊗-homo = record
+                  { F⇒G = record { MF.⊗-homo.⇒ }
+                  ; F⇐G = record { MF.⊗-homo.⇐ }
+                  ; iso = λ X → record { MF.⊗-homo.iso X }
+                  }
+              ; associativity = λ {X Y Z} → MF.associativity {X} {Y} {Z}
+              ; unitaryˡ = λ {X} → MF.unitaryˡ {X}
+              ; unitaryʳ = λ {X} → MF.unitaryʳ {X}
+              }
+          }
+
+  opaque
+
+    unfolding Sys-MC₁
+
+    Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC (Valuesₘ A)))
+    Sys-MC-identity {A} = record
+        { U = record
+            { F⇒G = record { ⇒ }
+            ; F⇐G = record { ⇐ }
+            ; iso = λ X → record { iso X}
+            }
+        ; F⇒G-isMonoidal = record
+            { ε-compat = ε-compat
+            ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X} {Y}
+            }
+        }
+      where
+        open MonoidalNaturalIsomorphism (Unlooped.NatMC.Sys.identity {A})
+
+    Sys-MC-homomorphism
+        : {g : Fin B → Fin C}
+          {f : Fin A → Fin B}
+        → MonoidalNaturalIsomorphism (Sys-MC₁ (g ∘ f)) (∘-StrongMonoidal (Sys-MC₁ g) (Sys-MC₁ f))
+    Sys-MC-homomorphism {g} {f} = record
+        { U = record
+            { F⇒G = record { ⇒ }
+            ; F⇐G = record { ⇐ }
+            ; iso = λ X → record { iso X}
+            }
+        ; F⇒G-isMonoidal = record
+            { ε-compat = ε-compat
+            ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X} {Y}
+            }
+        }
+      where
+        open MonoidalNaturalIsomorphism (Unlooped.NatMC.Sys.homomorphism {f = f} {g})
+
+    Sys-MC-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → MonoidalNaturalIsomorphism (Sys-MC₁ f) (Sys-MC₁ g)
+    Sys-MC-resp-≈ f≗g = record
+        { U = record
+            { F⇒G = record { ⇒ }
+            ; F⇐G = record { ⇐ }
+            ; iso = λ X → record { iso X}
+            }
+        ; F⇒G-isMonoidal = record
+            { ε-compat = ε-compat
+            ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X} {Y}
+            }
+        }
+      where
+        open MonoidalNaturalIsomorphism (Unlooped.NatMC.Sys.F-resp-≈ f≗g)
+
+  Sys : Functor Nat (StrongMonoidals (suc 0ℓ) 0ℓ 0ℓ)
+  Sys .F₀ = λ n → Systems-MC (Valuesₘ n)
+  Sys .F₁ = Sys-MC₁
+  Sys .identity = Sys-MC-identity
+  Sys .homomorphism = Sys-MC-homomorphism
+  Sys .F-resp-≈ = Sys-MC-resp-≈
+
+  module Sys = Functor Sys
+
+module NatSMC where
+
+  module _ (f : Fin A → Fin B) where
+
+    F-MF : StrongMonoidalFunctor (Systems-MC (Valuesₘ A)) (Systems-MC (Valuesₘ B))
+    F-MF = NatMC.Sys.₁ f
+    module F-MF = StrongMonoidalFunctor F-MF
+
+    module SMF = SymmetricMonoidalFunctor (Unlooped.NatSMC.Sys.₁ f)
+
+    opaque
+
+      unfolding NatMC.Sys-MC₁
+
+      Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC (Valuesₘ A)) (Systems-SMC (Valuesₘ B))
+      Sys-SMC₁ = record
+          { F-MF
+          ; isBraidedMonoidal = record
+              { F-MF
+              ; braiding-compat = λ {X Y} → SMF.braiding-compat {X} {Y}
+              }
+          }
+
+  opaque
+
+    unfolding Sys-SMC₁
+
+    Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC (Valuesₘ A)))
+    Sys-SMC-identity = record { MonoidalNaturalIsomorphism NatMC.Sys.identity }
+
+    Sys-SMC-homomorphism
+        : {g : Fin B → Fin C}
+          {f : Fin A → Fin B}
+        → SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ (g ∘ f)) (∘-StrongSymmetricMonoidal (Sys-SMC₁ g) (Sys-SMC₁ f))
+    Sys-SMC-homomorphism = record { MonoidalNaturalIsomorphism NatMC.Sys.homomorphism }
+
+    Sys-SMC-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → 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ℓ} {0ℓ} {0ℓ})
+    Sys .F₀ = λ n → Systems-SMC (Valuesₘ n)
+    Sys .F₁ = Sys-SMC₁
+    Sys .identity = Sys-SMC-identity
+    Sys .homomorphism = Sys-SMC-homomorphism
+    Sys .F-resp-≈ = Sys-SMC-resp-≈
+
+  module Sys = Functor Sys
+
+module NatCMon where
+
+  Sys : Functor Nat CMonoids
+  Sys = InducedCMonoid ∘F SymmetricMonoidalPreorder.Free ∘F NatSMC.Sys
+
+  module Sys = Functor Sys