Zulip Chat Archive

Stream: general

Topic: ulift instances


view this post on Zulip 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 }

view this post on Zulip Kenny Lau (Jun 14 2019 at 14:42):

can we automate this? is it worth it?

view this post on Zulip Reid Barton (Jun 14 2019 at 15:02):

It should be pretty much the same as pi_instances I think

view this post on Zulip Kevin Buzzard (Jun 14 2019 at 15:33):

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

view this post on Zulip Chris Hughes (Jun 14 2019 at 15:38):

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

view this post on Zulip Kevin Buzzard (Jun 14 2019 at 15:46):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jun 14 2019 at 17:10):

Would it have been easier to not use universes?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 16 2019 at 22:57):

You can do that in ZFC

view this post on Zulip Mario Carneiro (Jun 16 2019 at 22:58):

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

view this post on Zulip Kenny Lau (Jun 16 2019 at 23:04):

yeah this is a bit problematic for type theory

view this post on Zulip 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

view this post on Zulip 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