Zulip Chat Archive

Stream: general

Topic: How many universes did I use?

Kevin Buzzard (May 24 2018 at 19:49):

I proved a theorem in Lean (that an affine scheme is a scheme). Along the way I understood a little more about universes. In particular, I realised that the ZFC proof I knew that an affine scheme was a scheme "took place entirely within Type", by which I mean that every term I used was "good" -- here "good" is defined thus: (1) Type is good; (2) If X is a term of type Y and Y is good then X is good; (3) that's it. Once I realised this I went through a lot of files in my project that had lines of the form "universes u v w" and replaced them with "universe u", I also replaced many "Type v" and "Type *" with "Type u".

Kevin Buzzard (May 24 2018 at 19:49):

How do I check that I caught all of them?

Patrick Massot (May 24 2018 at 19:50):

What do you gain from these modifications?

Mario Carneiro (May 24 2018 at 19:56):

Agreed - these modifications do nothing toward your goal of eliminating unverse use

Mario Carneiro (May 24 2018 at 19:57):

What would help is using Type instead of Type u or Type*, but I don't recommend this

Chris Hughes (May 24 2018 at 19:57):

Doesn't changing Type v to Type u just make the theorem less general, and just worse?

Mario Carneiro (May 24 2018 at 19:58):

But your definition good is overly restrictive - ring is not good, not even ring.{0}, so ring A is also not good

Mario Carneiro (May 24 2018 at 19:59):

In fact clearly delineating what parts of DTT make sense in ZFC is rather delicate

Patrick Massot (May 24 2018 at 19:59):

We should have asked how many questions he marked before answering this thread

Kevin Buzzard (May 25 2018 at 09:59):

You're right that my definition of good is bad. I definitely don't want to put everything into Type because then other people won't want to use my code. But there is an underlying question here, and perhaps the answer is in Mario's comment "In fact clearly delineating what parts of DTT make sense in ZFC is rather delicate". I want to know the answer though. Is there any way I can find out whether my definition "would go through if I went through every file I used and removed all mention of universes, and changed all Type u and Type* to Type"?

Chris Hughes (May 25 2018 at 10:01):

It would go through, but nobody would be able to define a scheme structure on anything outside Type if I understand the question. So it would just be a less general definition.