chore(category_theory/sites/limits): generalise universe level (#16408)

leanprover-community · Sep 14, 2022 · 94b2c2c · 94b2c2c
1 parent 9532aeb
commit 94b2c2c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/category_theory/sites/limits.lean b/src/category_theory/sites/limits.lean
@@ -33,10 +33,10 @@ open opposite
 
 section limits
 
-universes w v u
+universes w v u z
 variables {C : Type (max v u)} [category.{v} C] {J : grothendieck_topology C}
 variables {D : Type w} [category.{max v u} D]
-variables {K : Type (max v u)} [small_category K]
+variables {K : Type z} [small_category K]
 
 noncomputable theory