dot universe notation

Stream: maths

[Juho Kupiainen]

What is the notation something.{v} where v is a universe? In category_theory/category/default in definition class category_struct for example this is used. Does this mean "{v} something" as usual? How should I think of this?

[Kevin Buzzard]

Can you post the actual definition of something from the library?

[Kevin Buzzard]

there will be some v inside the definition probably, and this might help to understand what's going on

[Kenny Lau]

they are the universes as inputs

[Johan Commelin]

@Juho Kupiainen No, the .{v} is not the same as .something dot notation

[Johan Commelin]

It just specifies explicitly: "Hey Lean, please use this universe, and not some random one"

[Mario Carneiro]

foo.{v} is like @foo v except it works with universe arguments instead of regular arguments