## Stream: maths

### Topic: dot universe notation

#### Juho Kupiainen (Sep 21 2020 at 09:15):

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 (Sep 21 2020 at 09:16):

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

#### Kevin Buzzard (Sep 21 2020 at 09:17):

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

#### Kenny Lau (Sep 21 2020 at 09:18):

they are the universes as inputs

#### Johan Commelin (Sep 21 2020 at 09:19):

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

#### Johan Commelin (Sep 21 2020 at 09:20):

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

#### Mario Carneiro (Sep 21 2020 at 13:51):

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

Last updated: May 09 2021 at 10:11 UTC