# Zulip Chat Archive

## Stream: general

### Topic: ulift instances

#### Kenny Lau (Jun 14 2019 at 14:42):

instance ulift.has_le {X : Type u} [has_le X] : has_le (ulift X) := ⟨λ x y, x.down ≤ y.down⟩ instance ulift.preorder {X : Type u} [preorder X] : preorder (ulift X) := { le_refl := λ x, le_refl x.down, le_trans := λ x y z, le_trans, .. ulift.has_le } instance ulift.partial_order {X : Type u} [partial_order X] : partial_order (ulift X) := { le_antisymm := λ x y hxy hyx, ulift.ext x y $ le_antisymm hxy hyx, le_trans := λ x y z, le_trans, .. ulift.preorder }

#### Kenny Lau (Jun 14 2019 at 14:42):

can we automate this? is it worth it?

#### Reid Barton (Jun 14 2019 at 15:02):

It should be pretty much the same as `pi_instances`

I think

#### Kevin Buzzard (Jun 14 2019 at 15:33):

You are a mathematician. Why do you need more than one universe?

#### Chris Hughes (Jun 14 2019 at 15:38):

@Kevin Buzzard didn't you use more than one universe to do valuations?

#### Kevin Buzzard (Jun 14 2019 at 15:46):

That's only because I was young and naive when writing that part of the code.

#### Kevin Buzzard (Jun 14 2019 at 15:47):

And in fact IIRC I spent a whole lot of time wrestling with a lemma which showed that any valuation on a ring taking values in a group in some random universe was equivalent to a valuation taking valuations in the same universe as the ring.

#### Chris Hughes (Jun 14 2019 at 17:10):

Would it have been easier to not use universes?

#### Kevin Buzzard (Jun 14 2019 at 17:19):

If we had made a blanket decision to only use one universe, *or* if we had decided to ignore Mario, then we would have had to write strictly less code. We had some structure `valuation (R : Type u)`

which had a field `Gamma : Type v`

except that Mario said that we'd run into trouble if we did it like that, so we went for `Gamma : Type u`

and then, at his suggestion, spent some time writing code which given a valuation on R (type u) taking values in Gamma (Type v) produced an equivalent valuation taking values in some other Gamma' (Type u). The type `Spv R`

was equivalence classes of valuations, so doing it all this way we were truly universe-polymorphic. However we never needed this extra polymorphism power.

What I am however unclear about is exactly how much was saved. Because I think that even if we'd stuck to Gamma : Type u we would have had issues with equivalence relations on things that "weren't sets" (in my model of this stuff) and might well have had to write some sort of code to fix this anyway (assuming that we wanted everything to live in Type u)

#### Chris Hughes (Jun 14 2019 at 17:23):

But `valuation (R : Type u) : Type (u+1)`

, so to actually not use universes you'd need to do more than stick to `Gamma : Type u`

#### Kevin Buzzard (Jun 14 2019 at 17:24):

Right but that just means that the class of all valuations isn't a set. I'm not bothered by that. I know what is a set and what is a class, and I don't need anything else. I won't be putting anything classy into a setty hole.

#### Kevin Buzzard (Jun 14 2019 at 17:25):

My general point is that I am not interested in what computer scientists think mathematics is, I am interested in what mathematicians think mathematics is, and they know how to do everything with just one universe.

#### Chris Hughes (Jun 14 2019 at 17:28):

I don't know enough ZFC to be sure exactly what you can do with classes, but I think I remember a set of the form `{x | ∃ Γ : Type, p Γ x}`

, which I don't think you can do in ZFC.

#### Mario Carneiro (Jun 16 2019 at 22:57):

You can do that in ZFC

#### Mario Carneiro (Jun 16 2019 at 22:58):

there are no classes involved there, that is just an unbounded quantification

#### Kenny Lau (Jun 16 2019 at 23:04):

yeah this is a bit problematic for type theory

#### Mario Carneiro (Jun 16 2019 at 23:07):

In most cases where I have seen this come up, you can prove that the existential quantification is equivalent to some predicative formulation, from which it follows that it is also equivalent to `{x | ∃ Γ : Type u, p Γ x}`

for arbitrary `u`

not in the original definition

#### Reid Barton (Jun 16 2019 at 23:16):

By "not in the original definition", do you mean bigger than everything else that appears?

Last updated: May 10 2021 at 19:16 UTC