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/Category.agda        |  63 ++++++++++++++++++++
 Data/System/Core.agda            |  84 +++++++++++++++++++++++++++
 Data/System/Looped.agda          |  83 +++++++++++++++++++++++++++
 Data/System/Looped/Monoidal.agda | 120 +++++++++++++++++++++++++++++++++++++++
 Data/System/Monoidal.agda        |  37 ++++++------
 5 files changed, 369 insertions(+), 18 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

(limited to 'Data/System')

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₂)
-- 
cgit v1.2.3