Zulip Chat Archive

Stream: maths

Topic: universal properties again


view this post on Zulip Patrick Massot (Jul 19 2018 at 20:29):

Since everybody is doing universal properties and fight reluctant universes and type class inference, let me try to get help. Remember I'm working with Hausdorff completions of uniform space. I have a nice proof of their universal properties and I'd like to run the usual stuff on it. Especially today I need uniqueness for this construction. So I forget about my explicit construction and try to run abstract arguments. See https://gist.github.com/PatrickMassot/beb3b40bec8888b3061d9c410c229467 First trouble: I had to setup explicit universe level in order to get Lean to accept compare. Then the instances buried in the structure are hard to get out. I guess I'm on a completely wrong track here.

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:51):

@Mario Carneiro I'm afraid you were busy typing some advertisement when that thread started (and stopped).

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:52):

Do you have any hint for me?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:57):

What explicit universe?

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:57):

u

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:58):

Oh yes that is true

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:58):

If I put Type* everywhere you see Type u I can shadowing errors

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:58):

Same if I try Type v for all beta variables

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:58):

That's the same thing I was talking about with Kevin

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:58):

the u in space : Type u is an internal universe variable

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:59):

so if you make it v instead then you will have a bad day

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:59):

so that means you have to explicitly make them the same, which means you need to name the variable

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:00):

same as who?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:00):

same as α : Type u

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:00):

I'm having a bad day even with named u

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:01):

At least I don't see .{u} anywhere in your file

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:01):

I get an error in uniform_continuous_compare?

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:01):

I'm fine with α and its completion living in the same universe. That sounds nice and is actually true for my explicit construction (I think)

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:01):

about synthesized instance different from inferred

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:01):

exactly, that's the heart of my question

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:02):

But why beta has to be in the same universe?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:02):

That's easy enough to fix, use letI instead of haveI

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:02):

Better yet, add this

attribute [instance]
  completion_package.uniform_structure
  completion_package.completeness
  completion_package.separation

and it won't be necessary

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:03):

beta is also an internal universe variable

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:04):

I'm sure I've seen this trick in the sheaf discussion, but I forgot. Thanks a lot

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:04):

it doesn't have to be in the sense that you can define it with a different variable, but this will make your life harder and furthermore it doesn't mean what you think it means

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:05):

It is impossible to define a field which quantifies over multiple universe levels

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:05):

I was worried I would have a lot of trouble with these instances but this trick seems to fix everything (including removing @uniform_continuous ugliness in the definition of compare)

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:05):

that is, something like this doesn't work: (lift : ∀ {u} {β : Type u} (f : α → β), space → β)

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:06):

where u is somehow quantified inside the structure

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:06):

What do you think I thought it meant and what would it actually mean? (Grammar clearly tell us we are in the middle of a tricky discussion involving multiple universes)

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:06):

Oh, (lift : ∀ {u} {β : Type u} (f : α → β), space → β) is what I would have liked to mean

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:07):

But I don't mind, really

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:07):

Luckily, in the vast majority of cases, having a lift in universe u implies a lift in higher universes too

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:07):

usually this is due to some zfc style size considerations

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:09):

I certainly don't want to run into zfc size considerations. Actually I mostly want to prove that the completion of a product is nicely isomorphic to the product of the completions, taking the opportunity to try abstract non-sense in Lean

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:11):

I think you should just stick to universe u

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:12):

it's not quite as strong a theorem as you could state, but all the constructions will go through without any added headache

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:14):

Great, I like that

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:14):

I'll try to move on. Thanks!


Last updated: May 18 2021 at 07:19 UTC