# increasing the universe level of a type in Lean by force

Given some term

A : Sort u


in Lean, is there a way to artificially increase the universe level and promote A to a term

A : Sort (u + 1)


in a higher universe?

Context: I have written down the definition of a large category in Lean.

structure Cat : Type 2 :=
(ob : Type 1)
(mor : Π p : ob × ob, Type 1)
(id : Π x : ob, mor(x,x))
(comp {x y z : ob} : Π g : mor(y,z), Π f : mor(x,y), mor(x,z))
(assoc {x y z w : ob} : ∀f : mor(x,y), ∀g : mor(y,z), ∀h : mor(z,w),
comp h (comp g f) = comp (comp h g) f)
(leftn {x y : ob} : ∀f : mor(x,y), comp (id y) f = f)
(rightn {x y : ob} : ∀f : mor(x,y), comp f (id x) = f)


Next I want to define a category SET of sets and a category PROP of propositions. The morphism types in the category of sets should be the standard function types, and the morphism types in the category of propositions should be implications.

Type : Type 1


is of the right universe level, but I have problems with the morphism types in SET and with both function and morphism types for PROP.

Prop : Type 0
φ : Prop, ψ : Prop ⊢ φ → ψ : Sort 0


The universe level is too low for my definition of a category. Is there a way to fix this without introducing different versions of Cat for different universe level combinations?

• ULift can raise universe levels, but I'd say this is usually not the best approach Aug 10 at 21:40
• Why not use universe variables instead of hard coding the level? Aug 11 at 3:02
• Here is the definition of semigroup in Mathlib. It uses universe levels for the carrier to specifically avoid your sort of problem. (It also uses a semi bundled approach where the carrier isn’t in the data of the structure.) This is pretty consistent throughout mathlib. Aug 11 at 13:25
• @JasonRute Thx! The thing is that even when I use universe levels, I will still have the problem that for SET the universe level of the morphism types will be 1 below that of the object type, while for other categories this isn't the case. But I guess I can just use two universes, right?
– Nico
Aug 11 at 13:35
• @Nico I might be misunderstanding, but you may want to try Sort u instead of Type u. Also I’d look at the existing category theory library starting with the definition of category to see how it compares to yours. Aug 11 at 14:43

You can define a universe polymorphic version of Cat.

universes u v

structure Cat : Type (max u v + 1) :=
(ob : Type u)
(mor : Π p : ob × ob, Type v)
(id : Π x : ob, mor(x,x))
(comp {x y z : ob} : Π g : mor(y,z), Π f : mor(x,y), mor(x,z))
(assoc {x y z w : ob} : ∀f : mor(x,y), ∀g : mor(y,z), ∀h : mor(z,w),
comp h (comp g f) = comp (comp h g) f)
(leftn {x y : ob} : ∀f : mor(x,y), comp (id y) f = f)
(rightn {x y : ob} : ∀f : mor(x,y), comp f (id x) = f)


If you ever need to specify universes explicitly you can write Cat.{u, v} for the Type of Categories with objects in u and morphisms in v. You could also define universe polymorphic versions of most of the well known categories, for example the category of Types could start something like this

def Types : Cat :=
{ ob := Type u,
mor := fun X, X.1 -> X.2,