From 5f4d1cf740591476d3c7bc270fd11a2c578ab7e6 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 5 Nov 2025 08:11:48 -0600
Subject: Adjust universe levels

---
 Functor/Monoidal/Construction/ListOf.agda     | 4 ++--
 Functor/Monoidal/Construction/MultisetOf.agda | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'Functor/Monoidal/Construction')

diff --git a/Functor/Monoidal/Construction/ListOf.agda b/Functor/Monoidal/Construction/ListOf.agda
index 476939e..23c6ba8 100644
--- a/Functor/Monoidal/Construction/ListOf.agda
+++ b/Functor/Monoidal/Construction/ListOf.agda
@@ -8,9 +8,9 @@ open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
 open import Level using (Level)
 
 module Functor.Monoidal.Construction.ListOf
-    {o ℓ e : Level}
+    {o o′ ℓ ℓ′ e e′ : Level}
     {𝒞 : CocartesianCategory o ℓ e}
-    {S : MonoidalCategory o ℓ e}
+    {S : MonoidalCategory o′ ℓ′ e′}
     (let module 𝒞 = CocartesianCategory 𝒞)
     (let module S = MonoidalCategory S)
     (G : Functor 𝒞.U S.U)
diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda
index 6862b84..eca7b3a 100644
--- a/Functor/Monoidal/Construction/MultisetOf.agda
+++ b/Functor/Monoidal/Construction/MultisetOf.agda
@@ -10,9 +10,9 @@ open import Category.Construction.CMonoids using (CMonoids)
 open import Level using (Level)
 
 module Functor.Monoidal.Construction.MultisetOf
-    {o ℓ e : Level}
+    {o o′ ℓ ℓ′ e e′ : Level}
     {𝒞 : CocartesianCategory o ℓ e}
-    {S : SymmetricMonoidalCategory o ℓ e}
+    {S : SymmetricMonoidalCategory o′ ℓ′ e′}
     (let module 𝒞 = CocartesianCategory 𝒞)
     (let module S = SymmetricMonoidalCategory S)
     (G : Functor 𝒞.U S.U)
-- 
cgit v1.2.3