From 9e2f3f3bb9916dca8d4ad4b162ce5b089c26b82e Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 13 Jul 2026 16:06:43 -0700
Subject: Construct Sys functor from wiring diagrams to Cats

---
 Data/System.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Data/System.agda')

diff --git a/Data/System.agda b/Data/System.agda
index 968332d..7b6fe06 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -2,9 +2,9 @@
 
 open import Level using (Level)
 
-module Data.System {ℓ : Level} where
+module Data.System {c ℓ : Level} where
 
-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)
+open import Data.System.Core {c} {ℓ} public
+open import Data.System.Category {c} {ℓ} public
+open import Data.System.Looped {c} {ℓ} public
+open import Data.System.Monoidal {c} {ℓ} public using (Systems-MC; Systems-SMC)
-- 
cgit v1.2.3