Coercion between universe levels

Stream: new members

[Coleton Kotch]

Given x : Type u I assume we should be able to get an associated x' : Type (u + 1).

This came up as I am looking at constructing a functor into Cat as follows,

def subobjectPresheaf [Limits.HasPullbacks C] : Functor Cᵒᵖ Cat.{u,v} where
  obj X := by
    letI := Cat.of <| Subobject X.unop
    --exact this
    sorry
  map f := sorry

uncommenting 'exact this', gives the following error:
type mismatch
this
has type
Cat : Type ((max u v) + 1)
but is expected to have type
Cat : Type (max (v + 1) v (u + 1))

This should not require being able to move up Type levels though as max (v + 1) v (u + 1) = (max u v) + 1, should hold unless I misunderstand some subtlety., but I am still curious if such an embedding exists.

The commented out subobjectPresheaf' does work, though I have not yet added simp lemmas to for aseop cat to check functoriality. I thought that a functor into Cat would be nice to have though given it would remember the functoriality of morphisms.

[Adam Topaz]

docs#ULift

[Coleton Kotch]

Adam Topaz said:

docs#ULift

Thanks!