Generalize systems to (co)commutative (co)monoids

5 files changed, 159 insertions, 137 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 }