universal properties again

Stream: maths

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

Do you have any hint for me?

[Mario Carneiro]

What explicit universe?

[Patrick Massot]

u

[Mario Carneiro]

Oh yes that is true

[Patrick Massot]

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

[Patrick Massot]

Same if I try Type v for all beta variables

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

same as who?

[Mario Carneiro]

same as α : Type u

[Patrick Massot]

I'm having a bad day even with named u

[Mario Carneiro]

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

[Mario Carneiro]

I get an error in uniform_continuous_compare?

[Patrick Massot]

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)

[Mario Carneiro]

about synthesized instance different from inferred

[Patrick Massot]

exactly, that's the heart of my question

[Patrick Massot]

But why beta has to be in the same universe?

[Mario Carneiro]

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

[Mario Carneiro]

Better yet, add this

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

and it won't be necessary

[Mario Carneiro]

beta is also an internal universe variable

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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)

[Mario Carneiro]

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

[Mario Carneiro]

where u is somehow quantified inside the structure

[Patrick Massot]

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)

[Patrick Massot]

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

[Patrick Massot]

But I don't mind, really

[Mario Carneiro]

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

[Mario Carneiro]

usually this is due to some zfc style size considerations

[Patrick Massot]

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

[Mario Carneiro]

I think you should just stick to universe u

[Mario Carneiro]

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

[Patrick Massot]

Great, I like that

[Patrick Massot]

I'll try to move on. Thanks!