0
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ ULift can raise universe levels, but I'd say this is usually not the best approach $\endgroup$
    – It'sNotALie.
    Commented Aug 10, 2023 at 21:40
  • 1
    $\begingroup$ Why not use universe variables instead of hard coding the level? $\endgroup$
    – Jason Rute
    Commented Aug 11, 2023 at 3:02
  • 1
    $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Commented Aug 11, 2023 at 13:25
  • $\begingroup$ @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? $\endgroup$
    – Nico
    Commented Aug 11, 2023 at 13:35
  • $\begingroup$ @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. $\endgroup$
    – Jason Rute
    Commented Aug 11, 2023 at 14:43

1 Answer 1

Reset to default
2
$\begingroup$

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,
Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.