From c65be5a260a44f35e26b771026153643ad2464b3 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sun, 11 Jan 2026 16:28:27 -0600
Subject: Construct SM nat trans from Circ to Sys

---
 Functor/Instance/Monoidalize.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Functor/Instance/Monoidalize.agda')

diff --git a/Functor/Instance/Monoidalize.agda b/Functor/Instance/Monoidalize.agda
index 6423109..b856f82 100644
--- a/Functor/Instance/Monoidalize.agda
+++ b/Functor/Instance/Monoidalize.agda
@@ -6,10 +6,10 @@ open import Categories.Category.Monoidal using (MonoidalCategory)
 open import Categories.Category.Cocartesian using (Cocartesian)
 
 module Functor.Instance.Monoidalize
-    {o o′ ℓ ℓ′ e e ′ : Level}
+    {o o′ ℓ ℓ′ e e′ : Level}
     {C : Category o ℓ e}
     (cocartesian : Cocartesian C)
-    (D : MonoidalCategory o ℓ e)
+    (D : MonoidalCategory o′ ℓ′ e′)
   where
 
 open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
-- 
cgit v1.2.3