From aada52132810a021a898f43daef5c90ced2a8bf0 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 14 Mar 2026 13:07:50 -0500
Subject: Refactor systems and add looped systems

---
 Data/System.agda                                  | 142 +---------------------
 Data/System/Category.agda                         |  63 ++++++++++
 Data/System/Core.agda                             |  84 +++++++++++++
 Data/System/Looped.agda                           |  83 +++++++++++++
 Data/System/Looped/Monoidal.agda                  | 120 ++++++++++++++++++
 Data/System/Monoidal.agda                         |  37 +++---
 Functor/Instance/Nat/System.agda                  |  86 +++++++------
 NaturalTransformation/Instance/GateSemantics.agda |  10 +-
 8 files changed, 421 insertions(+), 204 deletions(-)
 create mode 100644 Data/System/Category.agda
 create mode 100644 Data/System/Core.agda
 create mode 100644 Data/System/Looped.agda
 create mode 100644 Data/System/Looped/Monoidal.agda

diff --git a/Data/System.agda b/Data/System.agda
index a2adec3..968332d 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -1,142 +1,10 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ; suc)
+open import Level using (Level)
 
 module Data.System {ℓ : Level} where
 
-import Relation.Binary.Properties.Preorder as PreorderProperties
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-
-open import Categories.Category using (Category)
-open import Data.Circuit.Value using (Monoid)
-open import Data.Nat using (ℕ)
-open import Data.Setoid using (_⇒ₛ_; ∣_∣)
-open import Data.Setoid.Unit using (⊤ₛ)
-open import Data.Values Monoid using (Values; _≋_; module ≋; <ε>)
-open import Function using (Func; _⟨$⟩_; flip)
-open import Function.Construct.Constant using () renaming (function to Const)
-open import Function.Construct.Identity using () renaming (function to Id)
-open import Function.Construct.Setoid using (_∙_)
-open import Level using (Level; 0ℓ; suc)
-open import Relation.Binary as Rel using (Reflexive; Transitive; Preorder; Setoid; Rel)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-
-open Func
-
-module _ (n : ℕ) where
-
-  record System : Set₁ where
-
-    field
-      S : Setoid 0ℓ 0ℓ
-      fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
-      fₒ : ∣ S ⇒ₛ Values n ∣
-
-    fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
-    fₛ′ i = to (to fₛ i)
-
-    fₒ′ : ∣ S ∣ → ∣ Values n ∣
-    fₒ′ = to fₒ
-
-    module S = Setoid S
-
-  open System
-
-  discrete : System
-  discrete .S = ⊤ₛ
-  discrete .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ)
-  discrete .fₒ = Const ⊤ₛ (Values n) <ε>
-
-module _ {n : ℕ} where
-
-  record _≤_ (a b : System n) : Set ℓ where
-
-    private
-      module A = System a
-      module B = System b
-
-    open B using (S)
-
-    field
-      ⇒S : ∣ A.S ⇒ₛ B.S ∣
-      ≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) S.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
-      ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s)
-
-  infix 4 _≤_
-
-open System
-
-module _ {n : ℕ} where
-
-  open _≤_
-
-  ≤-refl : Reflexive (_≤_ {n})
-  ⇒S ≤-refl = Id _
-  ≗-fₛ (≤-refl {x}) _ _ = S.refl x
-  ≗-fₒ ≤-refl _ = ≋.refl
-
-  ≡⇒≤ : _≡_ Rel.⇒ _≤_
-  ≡⇒≤ ≡.refl = ≤-refl
-
-  ≤-trans : Transitive _≤_
-  ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
-  ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin
-      ⇒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 n) 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)) ∎
-
-  variable
-    A B C : System n
-
-  _≈_ : Rel (A ≤ B) 0ℓ
-  _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
-    where
-      module A⇒B = Setoid (S A ⇒ₛ S B)
-
-  open Rel.IsEquivalence
-
-  ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B})
-  ≈-isEquiv {B = B} .refl = S.refl B
-  ≈-isEquiv {B = B} .sym a = S.sym B a
-  ≈-isEquiv {B = B} .trans a b = S.trans B a b
-
-  ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h
-  ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin
-      ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩
-      ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩
-      ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎
-    where
-      open ≈-Reasoning (System.S C)
-
-System-≤ : ℕ → Preorder (suc 0ℓ) (suc 0ℓ) ℓ
-System-≤ n = record
-    { _≲_ = _≤_ {n}
-    ; isPreorder = record
-        { isEquivalence = ≡.isEquivalence
-        ; reflexive = ≡⇒≤
-        ; trans = ≤-trans
-        }
-    }
-
-Systemₛ : ℕ → Setoid (suc 0ℓ) ℓ
-Systemₛ n = PreorderProperties.InducedEquivalence (System-≤ n)
-
-Systems : ℕ → Category (suc 0ℓ) ℓ 0ℓ
-Systems n = record
-    { Obj = System n
-    ; _⇒_ = _≤_
-    ; _≈_ = _≈_
-    ; id = ≤-refl
-    ; _∘_ = flip ≤-trans
-    ; assoc = λ {D = D} → S.refl D
-    ; sym-assoc = λ {D = D} → S.refl D
-    ; identityˡ = λ {B = B} → S.refl B
-    ; identityʳ = λ {B = B} → S.refl B
-    ; identity² = λ {A = A} → S.refl A
-    ; equiv = ≈-isEquiv
-    ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i}
-    }
+open import Data.System.Core {ℓ} public
+open import Data.System.Category {ℓ} public
+open import Data.System.Looped {ℓ} public
+open import Data.System.Monoidal {ℓ} public using (Systems-MC; Systems-SMC)
diff --git a/Data/System/Category.agda b/Data/System/Category.agda
new file mode 100644
index 0000000..171a003
--- /dev/null
+++ b/Data/System/Category.agda
@@ -0,0 +1,63 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; 0ℓ; suc)
+
+module Data.System.Category {ℓ : Level} where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+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 Function using (Func; _⟨$⟩_; flip)
+open import Relation.Binary as Rel using (Setoid; Rel)
+
+open Func
+open System
+open _≤_
+
+private module ≈ {n m : ℕ} where
+
+  private
+    variable
+      A B C : System n m
+
+  _≈_ : Rel (A ≤ B) 0ℓ
+  _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
+    where
+      module A⇒B = Setoid (S A ⇒ₛ S B)
+
+  open Rel.IsEquivalence
+
+  ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B})
+  ≈-isEquiv {B = B} .refl = S.refl B
+  ≈-isEquiv {B = B} .sym a = S.sym B a
+  ≈-isEquiv {B = B} .trans a b = S.trans B a b
+
+  ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h
+  ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin
+      ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩
+      ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩
+      ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎
+    where
+      open ≈-Reasoning (System.S C)
+
+open ≈ using (_≈_) public
+open ≈ using (≈-isEquiv; ≤-resp-≈)
+
+Systems[_,_] : ℕ → ℕ → Category (suc 0ℓ) ℓ 0ℓ
+Systems[ n , m ] = record
+    { Obj = System n m
+    ; _⇒_ = _≤_
+    ; _≈_ = _≈_
+    ; id = ≤-refl
+    ; _∘_ = flip ≤-trans
+    ; assoc = λ {D = D} → S.refl D
+    ; sym-assoc = λ {D = D} → S.refl D
+    ; identityˡ = λ {B = B} → S.refl B
+    ; identityʳ = λ {B = B} → S.refl B
+    ; identity² = λ {A = A} → S.refl A
+    ; equiv = ≈-isEquiv
+    ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i}
+    }
diff --git a/Data/System/Core.agda b/Data/System/Core.agda
new file mode 100644
index 0000000..6da264c
--- /dev/null
+++ b/Data/System/Core.agda
@@ -0,0 +1,84 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; 0ℓ; suc)
+
+module Data.System.Core {ℓ : Level} where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Data.Circuit.Value using (Monoid)
+open import Data.Nat using (ℕ)
+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)
+open import Function.Construct.Setoid using (_∙_)
+open import Relation.Binary using (Setoid; Reflexive; Transitive)
+
+open Func
+
+-- A dynamical system with a set of states,
+-- a state update function,
+-- and a readout function
+record System (n m : ℕ) : Set₁ where
+
+  field
+    S : Setoid 0ℓ 0ℓ
+    fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
+    fₒ : ∣ S ⇒ₛ Values m ∣
+
+  fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
+  fₛ′ i = to (to fₛ i)
+
+  fₒ′ : ∣ S ∣ → ∣ Values m ∣
+  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 _ {n m : ℕ} where
+
+  -- Simulation of systems: a mapping of internal
+  -- states which respects i/o behavior
+  record _≤_ (A B : System n m) : Set ℓ where
+
+    private
+      module A = System A
+      module B = System B
+
+    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)
+
+  infix 4 _≤_
+
+  open _≤_
+  open System
+
+  -- ≤ is reflexive: every system simulates itself
+  ≤-refl : Reflexive _≤_
+  ⇒S ≤-refl = Id _
+  ≗-fₛ (≤-refl {x}) _ _ = S.refl x
+  ≗-fₒ ≤-refl _ = ≋.refl
+
+  -- ≤ is transitive: if B simulates A, and C simulates B, then C simulates A
+  ≤-trans : Transitive _≤_
+  ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
+  ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin
+      ⇒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ₒ′ 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
new file mode 100644
index 0000000..f69d75b
--- /dev/null
+++ b/Data/System/Looped.agda
@@ -0,0 +1,83 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; 0ℓ; suc)
+
+module Data.System.Looped {ℓ : Level} where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+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 Function using (Func; _⟨$⟩_) renaming (id to idf)
+
+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
+
+  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
+
+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
+    }
+
+module _ (n : ℕ) where
+
+  open Category Systems[ n , n ]
+  open Functor (Loop n)
+
+  Systems[_] : Category (suc 0ℓ) ℓ 0ℓ
+  Systems[_] = categoryHelper record
+      { Obj = Obj
+      ; _⇒_ = _⇒_
+      ; _≈_ = λ f g → F₁ f ≈ F₁ g
+      ; id = id
+      ; _∘_ = _∘_
+      ; assoc = λ {f = f} {g h} → assoc {f = f} {g} {h}
+      ; identityˡ = λ {A B f} → identityˡ {A} {B} {f}
+      ; identityʳ = λ {A B f} → identityʳ {A} {B} {f}
+      ; equiv = equiv
+      ; ∘-resp-≈ = λ {f = f} {g h i} f≈g h≈i → ∘-resp-≈ {f = f} {g} {h} {i} f≈g h≈i
+      }
diff --git a/Data/System/Looped/Monoidal.agda b/Data/System/Looped/Monoidal.agda
new file mode 100644
index 0000000..af3d77c
--- /dev/null
+++ b/Data/System/Looped/Monoidal.agda
@@ -0,0 +1,120 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; 0ℓ; suc)
+
+module Data.System.Looped.Monoidal {ℓ : Level} where
+
+import Categories.Morphism as Morphism
+import Data.System.Monoidal {ℓ} as Unlooped
+
+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[_])
+
+module _ (n : ℕ) where
+
+  private
+
+    module Systems-MC = MonoidalCategory (Unlooped.Systems-MC n n)
+
+    ⊗ : Bifunctor Systems[ n ] Systems[ n ] Systems[ n ]
+    ⊗ = record
+        { F₀ = Systems-MC.⊗.₀
+        ; F₁ = Systems-MC.⊗.₁
+        ; identity = λ {X} → Systems-MC.⊗.identity {X}
+        ; homomorphism = λ {f = f} {g} → Systems-MC.⊗.homomorphism {f = f} {g}
+        ; F-resp-≈ = λ {f = f} {g} → Systems-MC.⊗.F-resp-≈ {f = f} {g}
+        }
+
+    module _ {X : System n n} where
+
+      open Morphism Systems[ n ] using (_≅_; module Iso)
+      open Systems-MC using (_⊗₀_)
+
+      unitorˡ : Systems-MC.unit ⊗₀ X ≅ X
+      unitorˡ = record
+          { from = Systems-MC.unitorˡ.from
+          ; to = Systems-MC.unitorˡ.to
+          ; iso = record
+              { isoˡ = Systems-MC.unitorˡ.isoˡ {X}
+              ; isoʳ = Systems-MC.unitorˡ.isoʳ {X}
+              }
+          }
+
+      unitorʳ : X ⊗₀ Systems-MC.unit ≅ X
+      unitorʳ = record
+          { from = Systems-MC.unitorʳ.from
+          ; to = Systems-MC.unitorʳ.to
+          ; iso = record
+              { isoˡ = Systems-MC.unitorʳ.isoˡ {X}
+              ; isoʳ = Systems-MC.unitorʳ.isoʳ {X}
+              }
+          }
+
+    module _ {X Y Z : System n n} where
+
+      module X = System X
+      module Y = System Y
+      module Z = System Z
+
+      open Morphism Systems[ n ] using (_≅_; module Iso)
+      open Systems-MC using (_⊗₀_)
+
+      associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)
+      associator = record
+          { from = Systems-MC.associator.from
+          ; to = Systems-MC.associator.to
+          ; iso = record
+              { isoˡ = Systems-MC.associator.isoˡ {X} {Y} {Z}
+              ; isoʳ = Systems-MC.associator.isoʳ {X} {Y} {Z}
+              }
+          }
+
+  Systems-Monoidal : Monoidal Systems[ n ]
+  Systems-Monoidal = record
+      { ⊗ = ⊗
+      ; unit = Systems-MC.unit
+      ; unitorˡ = unitorˡ
+      ; unitorʳ = unitorʳ
+      ; associator = associator
+      ; unitorˡ-commute-from = λ {f = f} → Systems-MC.unitorˡ-commute-from {f = f}
+      ; unitorˡ-commute-to = λ {f = f} → Systems-MC.unitorˡ-commute-to {f = f}
+      ; unitorʳ-commute-from = λ {f = f} → Systems-MC.unitorʳ-commute-from {f = f}
+      ; unitorʳ-commute-to = λ {f = f} → Systems-MC.unitorʳ-commute-to {f = f}
+      ; assoc-commute-from = λ {f = f} {g = g} {h = h} → Systems-MC.assoc-commute-from {f = f} {g = g} {h = h}
+      ; assoc-commute-to = λ {f = f} {g = g} {h = h} → Systems-MC.assoc-commute-to {f = f} {g = g} {h = h}
+      ; triangle = λ {X Y} → Systems-MC.triangle {X} {Y}
+      ; pentagon = λ {X Y Z W} → Systems-MC.pentagon {X} {Y} {Z} {W}
+      }
+
+  private
+
+    module Systems-SMC = SymmetricMonoidalCategory (Unlooped.Systems-SMC n n)
+
+    braiding : ⊗ ≃ flip-bifunctor ⊗
+    braiding = record
+        { F⇒G = record { Systems-SMC.braiding.⇒ }
+        ; F⇐G = record { Systems-SMC.braiding.⇐ }
+        ; iso = λ X → record { Systems-SMC.braiding.iso X }
+        }
+
+  Systems-Symmetric : Symmetric Systems-Monoidal
+  Systems-Symmetric = record
+      { braided = record
+          { braiding = braiding
+          ; hexagon₁ = λ {X Y Z} → Systems-SMC.hexagon₁ {X} {Y} {Z}
+          ; hexagon₂ = λ {X Y Z} → Systems-SMC.hexagon₂ {X} {Y} {Z}
+          }
+      ; commutative = λ {X Y} → Systems-SMC.commutative {X} {Y}
+      }
+
+  Systems-MC : MonoidalCategory (suc 0ℓ) ℓ 0ℓ
+  Systems-MC = record { monoidal = Systems-Monoidal }
+
+  Systems-SMC : SymmetricMonoidalCategory (suc 0ℓ) ℓ 0ℓ
+  Systems-SMC = record { symmetric = Systems-Symmetric }
diff --git a/Data/System/Monoidal.agda b/Data/System/Monoidal.agda
index 31b6c20..731bbe5 100644
--- a/Data/System/Monoidal.agda
+++ b/Data/System/Monoidal.agda
@@ -3,16 +3,17 @@
 open import Data.Nat using (ℕ)
 open import Level using (Level; suc; 0ℓ)
 
-module Data.System.Monoidal {ℓ : Level} (n : ℕ) where
+module Data.System.Monoidal {ℓ : Level} (n m : ℕ) where
 
-open import Data.System {ℓ} using (System; Systems; _≤_; ≤-refl; ≤-trans; _≈_; discrete)
+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.Functor using (Functor)
 open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor)
-open import Categories.Morphism (Systems n) using (_≅_; Iso)
+open import Categories.Morphism (Systems[ n , m ]) using (_≅_; Iso)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
 open import Data.Circuit.Value using (Monoid)
 open import Data.Product using (_,_; _×_; uncurry′)
@@ -35,11 +36,11 @@ module _ where
   δₛ .to v = v , v
   δₛ .cong v≋w = v≋w , v≋w
 
-  ⊕ₛ : Values n ×ₛ Values n ⟶ₛ Values n
+  ⊕ₛ : Values m ×ₛ Values m ⟶ₛ Values m
   ⊕ₛ .to (v , w) = v ⊕ w
   ⊕ₛ .cong (v₁≋v₂ , w₁≋w₂) = ⊕-cong v₁≋v₂ w₁≋w₂
 
-_⊗₀_ : System n → System n → System n
+_⊗₀_ : System n m → System n m → System n m
 _⊗₀_ X Y = let open System in record
     { S = S X ×ₛ S Y
     ; fₛ = fₛ X ×-⇒ fₛ Y ∙ δₛ
@@ -47,7 +48,7 @@ _⊗₀_ X Y = let open System in record
     }
 
 _⊗₁_
-    : {A A′ B B′ : System n}
+    : {A A′ B B′ : System n m}
       (f : A ≤ A′)
       (g : B ≤ B′)
     → A ⊗₀ B ≤ A′ ⊗₀ B′
@@ -60,33 +61,33 @@ module _ where
   open Functor
   open System
 
-  ⊗ : Bifunctor (Systems n) (Systems n) (Systems n)
+  ⊗ : Bifunctor Systems[ n , m ] Systems[ n , m ] Systems[ n , m ]
   ⊗ .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} where
+module Unitors {X : System n m} where
 
   open System X
 
-  ⊗-discreteˡ-≤ : discrete n ⊗₀ X ≤ X
+  ⊗-discreteˡ-≤ : discrete n m ⊗₀ X ≤ X
   ⊗-discreteˡ-≤ .⇒S = proj₂ₛ
   ⊗-discreteˡ-≤ .≗-fₛ i s = S.refl
   ⊗-discreteˡ-≤ .≗-fₒ (_ , s) = ⊕-identityˡ (fₒ′ s)
 
-  ⊗-discreteˡ-≥ : X ≤ discrete n ⊗₀ X
+  ⊗-discreteˡ-≥ : X ≤ discrete n m ⊗₀ 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ʳ-≤ : X ⊗₀ discrete n ≤ X
+  ⊗-discreteʳ-≤ : X ⊗₀ discrete n m ≤ X
   ⊗-discreteʳ-≤ .⇒S = proj₁ₛ
   ⊗-discreteʳ-≤ .≗-fₛ i s = S.refl
   ⊗-discreteʳ-≤ .≗-fₒ (s , _) = ⊕-identityʳ (fₒ′ s)
 
-  ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete n
+  ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete n m
   ⊗-discreteʳ-≥ .⇒S = record { to = λ s → s , _ ; cong = λ s≈s′ → s≈s′ , _ }
   ⊗-discreteʳ-≥ .≗-fₛ i s = S.refl , _
   ⊗-discreteʳ-≥ .≗-fₒ s = ≋.sym (⊕-identityʳ (fₒ′ s))
@@ -94,13 +95,13 @@ module Unitors {X : System n} where
   open _≅_
   open Iso
 
-  unitorˡ : discrete n ⊗₀ X ≅ X
+  unitorˡ : discrete n m ⊗₀ X ≅ X
   unitorˡ .from = ⊗-discreteˡ-≤
   unitorˡ .to = ⊗-discreteˡ-≥
   unitorˡ .iso .isoˡ = _ , S.refl
   unitorˡ .iso .isoʳ = S.refl
 
-  unitorʳ : X ⊗₀ discrete n ≅ X
+  unitorʳ : X ⊗₀ discrete n m ≅ X
   unitorʳ .from = ⊗-discreteʳ-≤
   unitorʳ .to = ⊗-discreteʳ-≥
   unitorʳ .iso .isoˡ = S.refl , _
@@ -108,7 +109,7 @@ module Unitors {X : System n} where
 
 open Unitors using (unitorˡ; unitorʳ) public
 
-module Associator {X Y Z : System n} where
+module Associator {X Y Z : System n m} where
 
   module X = System X
   module Y = System Y
@@ -135,10 +136,10 @@ module Associator {X Y Z : System n} where
 
 open Associator using (associator) public
 
-Systems-Monoidal : Monoidal (Systems n)
+Systems-Monoidal : Monoidal Systems[ n , m ]
 Systems-Monoidal = let open System in record
     { ⊗ = ⊗
-    ; unit = discrete n
+    ; unit = discrete n m
     ; unitorˡ = unitorˡ
     ; unitorʳ = unitorʳ
     ; associator = associator
@@ -154,7 +155,7 @@ Systems-Monoidal = let open System in record
 
 open System
 
-⊗-swap-≤ : {X Y : System n} → Y ⊗₀ X ≤ X ⊗₀ Y
+⊗-swap-≤ : {X Y : System n m} → 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₂)
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index a3c65ca..35768f8 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -35,8 +35,7 @@ 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; _≤_; Systemₛ; Systems; ≤-refl; ≤-trans; _≈_; discrete)
-open import Data.System.Monoidal {suc 0ℓ} using (Systems-MC; Systems-SMC)
+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 Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
 open import Function.Construct.Identity using () renaming (function to Id)
@@ -63,7 +62,7 @@ private
 
 opaque
   unfolding Valuesₘ ≋-isEquiv
-  map : (Fin A → Fin B) → System A → System B
+  map : (Fin A → Fin B) → System A A → System B B
   map {A} {B} f X = let open System X in record
       { S = S
       ; fₛ = fₛ ∙ arr (Pull.₁ f)
@@ -73,7 +72,7 @@ opaque
 opaque
   unfolding map
   open System
-  map-≤ : (f : Fin A → Fin B) {X Y : System A} → X ≤ Y → map f X ≤ map f Y
+  map-≤ : (f : Fin A → Fin B) {X Y : System A 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
@@ -82,15 +81,15 @@ opaque
   unfolding map-≤
   map-≤-refl
       : (f : Fin A → Fin B)
-      → {X : System A}
-      → map-≤ f (≤-refl {A} {X}) ≈ ≤-refl
+      → {X : System A A}
+      → map-≤ f (≤-refl {A} {A} {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}
+      → {X Y Z : System A A}
       → {h : X ≤ Y}
       → {g : Y ≤ Z}
       → map-≤ f (≤-trans h g) ≈ ≤-trans (map-≤ f h) (map-≤ f g)
@@ -100,13 +99,13 @@ opaque
   unfolding map-≤
   map-≈
       : (f : Fin A → Fin B)
-      → {X Y : System A}
+      → {X Y : System A 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) (Systems B)
+Sys₁ : (Fin A → Fin B) → Functor Systems[ A , A ] Systems[ B , B ]
 Sys₁ {A} {B} f = record
     { F₀ = map f
     ; F₁ = λ C≤D → map-≤ f C≤D
@@ -117,14 +116,14 @@ Sys₁ {A} {B} f = record
 
 opaque
   unfolding map
-  map-id-≤ : (X : System A) → map id X ≤ X
+  map-id-≤ : (X : System A 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) → X ≤ map id X
+  map-id-≥ : (X : System A 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
@@ -132,7 +131,7 @@ opaque
 opaque
   unfolding map-≤ map-id-≤
   map-id-comm
-      : {X Y : System A}
+      : {X Y : System A 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)
@@ -142,12 +141,12 @@ opaque
   unfolding map-id-≤ map-id-≥
 
   map-id-isoˡ
-      : (X : System A)
+      : (X : System A A)
       → ≤-trans (map-id-≤ X) (map-id-≥ X) ≈ ≤-refl
   map-id-isoˡ X = Setoid.refl (S X)
 
   map-id-isoʳ
-      : (X : System A)
+      : (X : System A A)
       → ≤-trans (map-id-≥ X) (map-id-≤ X) ≈ ≤-refl
   map-id-isoʳ X = Setoid.refl (S X)
 
@@ -167,7 +166,7 @@ opaque
   map-∘-≤
       : (f : Fin A → Fin B)
         (g : Fin B → Fin C)
-        (X : System A)
+        (X : System A 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
@@ -178,7 +177,7 @@ opaque
   map-∘-≥
       : (f : Fin A → Fin B)
         (g : Fin B → Fin C)
-        (X : System A)
+        (X : System A 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)
@@ -203,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}
+          → {X Y : System A 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) where
+    module _ (X : System A A) where
       opaque
         unfolding map-∘-≤ map-∘-≥
         isoˡ : ≤-trans (map-∘-≤ f g X) (map-∘-≥ f g X) ≈ ≤-refl
@@ -216,8 +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) where
+module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System A A) where
 
   opaque
 
@@ -238,7 +236,7 @@ opaque
   map-cong-comm
       : {f g : Fin A → Fin B}
         (f≗g : f ≗ g)
-        {X Y : System A}
+        {X Y : System A A}
         (h : X ≤ Y)
       → ≤-trans (map-≤ f h) (map-cong-≤ f≗g Y)
       ≈ ≤-trans (map-cong-≤ f≗g X) (map-≤ g h)
@@ -251,14 +249,14 @@ opaque
   map-cong-isoˡ
       : {f g : Fin A → Fin B}
         (f≗g : f ≗ g)
-        (X : System A)
+        (X : System A 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)
+        (X : System A A)
       → ≤-trans (map-cong-≥ f≗g X) (map-cong-≤ f≗g X) ≈ ≤-refl
   map-cong-isoʳ f≗g X = Setoid.refl (S X)
 
@@ -276,7 +274,7 @@ Sys-resp-≈ f≗g = niHelper record
 module NatCat where
 
   Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ)
-  Sys .F₀ = Systems
+  Sys .F₀ n = Systems[ n , n ]
   Sys .F₁ = Sys₁
   Sys .identity = Sys-identity
   Sys .homomorphism = Sys-homo _ _
@@ -288,15 +286,15 @@ module NatMC where
 
   module _ (f : Fin A → Fin B) where
 
-    module A = System-⊗ A
-    module B = System-⊗ B
+    module A = System-⊗ A A
+    module B = System-⊗ B B
 
     open CommutativeMonoid⇒ (Push.₁ f)
-    open Morphism (Systems B) using (_≅_)
+    open Morphism Systems[ B , B ] using (_≅_)
 
     opaque
       unfolding map
-      ε-≅ : discrete B ≅ map f (discrete A)
+      ε-≅ : discrete B B ≅ map f (discrete A A)
       ε-≅ = record
           -- other fields can be inferred
           { from = record
@@ -337,7 +335,7 @@ module NatMC where
       module A-MC = MonoidalCategory A.Systems-MC
       module B-MC = MonoidalCategory B.Systems-MC
 
-      F : Functor (Systems A) (Systems B)
+      F : Functor Systems[ A , A ] Systems[ B , B ]
       F = Sys₁ f
 
       module F = Functor F
@@ -349,7 +347,7 @@ module NatMC where
       unfolding ⊗-homo-≃
 
       associativity
-          : {X Y Z : System A}
+          : {X Y Z : System A A}
           → F.₁ A.Associator.assoc-≤
           ∘′ ⊗-homo-≃.⇒.η (X A.⊗₀ Y , Z)
           ∘′ ⊗-homo-≃.⇒.η (X , Y) B.⊗₁ B-MC.id
@@ -359,7 +357,7 @@ module NatMC where
       associativity {X} {Y} {Z} = Setoid.refl (S X ×ₛ (S Y ×ₛ S Z))
 
       unitaryˡ
-          : {X : System A}
+          : {X : System A A}
           →  F.₁ A.Unitors.⊗-discreteˡ-≤
           ∘′ ⊗-homo-≃.⇒.η (A-MC.unit , X)
           ∘′ ε-≅.from B.⊗₁ B-MC.id 
@@ -367,14 +365,14 @@ module NatMC where
       unitaryˡ {X} = Setoid.refl (S X)
 
       unitaryʳ
-          : {X : System A}
+          : {X : System A A}
           →  F.₁ A.Unitors.⊗-discreteʳ-≤
-          ∘′ ⊗-homo-≃.⇒.η (X , discrete A)
+          ∘′ ⊗-homo-≃.⇒.η (X , discrete A A)
           ∘′ B-MC.id B.⊗₁ ε-≅.from
           B-MC.≈ B-MC.unitorʳ.from
       unitaryʳ {X} = Setoid.refl (S X)
 
-    Sys-MC₁ : StrongMonoidalFunctor (Systems-MC A) (Systems-MC B)
+    Sys-MC₁ : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B)
     Sys-MC₁ = record
         { F = Sys₁ f
         ; isStrongMonoidal = record
@@ -388,7 +386,7 @@ module NatMC where
 
   opaque
     unfolding map-id-≤ ⊗-homo-≃
-    Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC A))
+    Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC A A))
     Sys-MC-identity = record
         { U = NatCat.Sys.identity
         ; F⇒G-isMonoidal = record
@@ -426,7 +424,7 @@ module NatMC where
         }
 
   Sys : Functor Nat (StrongMonoidals (suc 0ℓ) (suc 0ℓ) 0ℓ)
-  Sys .F₀ = Systems-MC
+  Sys .F₀ n = Systems-MC n n
   Sys .F₁ = Sys-MC₁
   Sys .identity = Sys-MC-identity
   Sys .homomorphism = Sys-MC-homomorphism
@@ -440,29 +438,29 @@ module NatSMC where
 
     private
 
-      module A = System-⊗ A
-      module B = System-⊗ B
+      module A = System-⊗ A A
+      module B = System-⊗ B B
       module A-SMC = SymmetricMonoidalCategory A.Systems-SMC
       module B-SMC = SymmetricMonoidalCategory B.Systems-SMC
 
-      F : Functor (Systems A) (Systems B)
+      F : Functor Systems[ A , A ] Systems[ B , B ]
       F = Sys₁ f
 
       module F = Functor F
 
-      F-MF : StrongMonoidalFunctor (Systems-MC A) (Systems-MC B)
+      F-MF : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B)
       F-MF = NatMC.Sys.₁ f
       module F-MF = StrongMonoidalFunctor F-MF
 
     opaque
       unfolding NatMC.⊗-homo-≃
       σ-compat
-          : {X Y : System A}
+          : {X Y : System A 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) (Systems-SMC B)
+    Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC A A) (Systems-SMC B B)
     Sys-SMC₁ = record
         { F-MF
         ; isBraidedMonoidal = record
@@ -471,7 +469,7 @@ module NatSMC where
             }
         }
 
-  Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC A))
+  Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC A A))
   Sys-SMC-identity = record { MonoidalNaturalIsomorphism NatMC.Sys.identity }
 
   Sys-SMC-homomorphism
@@ -487,7 +485,7 @@ module NatSMC where
   Sys-SMC-resp-≈ f≗g = record { MonoidalNaturalIsomorphism (NatMC.Sys.F-resp-≈ f≗g) }
 
   Sys : Functor Nat (SymMonCat {suc 0ℓ} {suc 0ℓ} {0ℓ})
-  Sys .F₀ = Systems-SMC
+  Sys .F₀ n = Systems-SMC n n
   Sys .F₁ = Sys-SMC₁
   Sys .identity = Sys-SMC-identity
   Sys .homomorphism = Sys-SMC-homomorphism
diff --git a/NaturalTransformation/Instance/GateSemantics.agda b/NaturalTransformation/Instance/GateSemantics.agda
index c85526c..9cdbc1b 100644
--- a/NaturalTransformation/Instance/GateSemantics.agda
+++ b/NaturalTransformation/Instance/GateSemantics.agda
@@ -44,12 +44,12 @@ opaque
 
   unfolding Values
 
-  1-cell : Value → System 1
+  1-cell : Value → System 1 1
   1-cell x .S = ⊤ₛ
   1-cell x .fₛ = Const (Values 1) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ)
   1-cell x .fₒ = Const ⊤ₛ (Values 1) λ { 0F → x }
 
-  2-cell : (Value → Value) → System 2
+  2-cell : (Value → Value) → System 2 2
   2-cell f .S = Valueₛ
   2-cell f .fₛ .to x = Const Valueₛ Valueₛ (f (x (# 0)))
   2-cell f .fₛ .cong x = ≡.cong f (x (# 0))
@@ -58,7 +58,7 @@ opaque
   2-cell f .fₒ .cong _ 0F = ≡.refl
   2-cell f .fₒ .cong x 1F = x
 
-  3-cell : (Value → Value → Value) → System 3
+  3-cell : (Value → Value → Value) → System 3 3
   3-cell f .S = Valueₛ
   3-cell f .fₛ .to i = Const Valueₛ Valueₛ (f (i (# 0)) (i (# 1)))
   3-cell f .fₛ .cong ≡i = ≡.cong₂ f (≡i (# 0)) (≡i (# 1))
@@ -125,7 +125,7 @@ module _ where
   open Belnap
   open Gate
 
-  system-of-gate : {n : ℕ} → Gate n → System n
+  system-of-gate : {n : ℕ} → Gate n → System n n
   system-of-gate ZERO = 1-cell true
   system-of-gate ONE  = 1-cell false
   system-of-gate ID   = 2-cell id
@@ -147,7 +147,7 @@ private
 
 open EGate hiding (Edge)
 
-system-of-edge : {n : ℕ} → ∣ Edge.₀ n ∣ → System n
+system-of-edge : {n : ℕ} → ∣ Edge.₀ n ∣ → System n n
 system-of-edge (mkEdge gate ports) = U.₁ (Sys.₁ ports) ⟨$⟩ system-of-gate gate
 
 system-of-edgeₛ : (n : ℕ) → Edge.₀ n ⟶ₛ U.₀ (Sys.₀ n)
-- 
cgit v1.2.3