ulift instances

Stream: general

[Kenny Lau]

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]

can we automate this? is it worth it?

[Reid Barton]

It should be pretty much the same as pi_instances I think

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Would it have been easier to not use universes?

[Kevin Buzzard]

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]

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]

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]

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]

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]

You can do that in ZFC

[Mario Carneiro]

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

[Kenny Lau]

yeah this is a bit problematic for type theory

[Mario Carneiro]

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]

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