Zulip Chat Archive

Stream: maths

Topic: dot universe notation


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 09:16):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 21 2020 at 09:18):

they are the universes as inputs

view this post on Zulip Johan Commelin (Sep 21 2020 at 09:19):

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

view this post on Zulip Johan Commelin (Sep 21 2020 at 09:20):

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

view this post on Zulip 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