## Stream: maths

### Topic: universal properties again

#### 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.

#### Patrick Massot (Jul 19 2018 at 20:52):

Do you have any hint for me?

#### Mario Carneiro (Jul 19 2018 at 20:57):

What explicit universe?

u

#### Mario Carneiro (Jul 19 2018 at 20:58):

Oh yes that is true

#### Patrick Massot (Jul 19 2018 at 20:58):

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

#### Patrick Massot (Jul 19 2018 at 20:58):

Same if I try Type v for all beta variables

#### Mario Carneiro (Jul 19 2018 at 20:58):

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

#### Mario Carneiro (Jul 19 2018 at 20:58):

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

#### Mario Carneiro (Jul 19 2018 at 20:59):

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

#### 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

same as who?

#### Mario Carneiro (Jul 19 2018 at 21:00):

same as α : Type u

#### Patrick Massot (Jul 19 2018 at 21:00):

I'm having a bad day even with named u

#### Mario Carneiro (Jul 19 2018 at 21:01):

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

#### Mario Carneiro (Jul 19 2018 at 21:01):

I get an error in uniform_continuous_compare?

#### 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)

#### Mario Carneiro (Jul 19 2018 at 21:01):

about synthesized instance different from inferred

#### Patrick Massot (Jul 19 2018 at 21:01):

exactly, that's the heart of my question

#### Patrick Massot (Jul 19 2018 at 21:02):

But why beta has to be in the same universe?

#### Mario Carneiro (Jul 19 2018 at 21:02):

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

#### Mario Carneiro (Jul 19 2018 at 21:02):

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


and it won't be necessary

#### Mario Carneiro (Jul 19 2018 at 21:03):

beta is also an internal universe variable

#### 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

#### 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

#### Mario Carneiro (Jul 19 2018 at 21:05):

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

#### 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)

#### Mario Carneiro (Jul 19 2018 at 21:05):

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

#### Mario Carneiro (Jul 19 2018 at 21:06):

where u is somehow quantified inside the structure

#### 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)

#### Patrick Massot (Jul 19 2018 at 21:06):

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

#### Patrick Massot (Jul 19 2018 at 21:07):

But I don't mind, really

#### 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

#### Mario Carneiro (Jul 19 2018 at 21:07):

usually this is due to some zfc style size considerations

#### 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

#### Mario Carneiro (Jul 19 2018 at 21:11):

I think you should just stick to universe u

#### 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

#### Patrick Massot (Jul 19 2018 at 21:14):

Great, I like that

#### Patrick Massot (Jul 19 2018 at 21:14):

I'll try to move on. Thanks!

Last updated: May 18 2021 at 07:19 UTC