universal properties and universes

Stream: new members

[Cameron Torrance]

I'm writing a commutative ring library (in lean 3) and have come up a against a problem with working with universal properties. This is the code I'm using to define final rings:

def final_ring : (Σ R : Type u, comm_ring R) → Prop
  | ⟨R,lR⟩ := ∀ pair : (Σ R' : Type v, comm_ring R'), ∃! ψ : @ring_hom pair.1  R  pair.2 lR , true

Using this definition it is fairly easy to show the zero ring is final. But I run into problems when using it to prove that a final ring is unique since a new universe variable is introduced with each assumption of the form final_ring Z and there seem to be no way to force it to be a particular universe. Is there any way around this or should be just saying that a universal property holds for rings in a particular universe?

[Eric Wieser]

Can you elaborate on the problem, perhaps with an example?

[Eric Wieser]

Are you aware of the [final_ring.{u v} Z] notation that lets you provide the value of the universe variables explicitly?

[Eric Wieser]

(also, ∃! ψ : @ring_hom pair.1 R pair.2 lR , true is possibly better spelt nonempty (unique (@ring_hom pair.1 R pair.2 lR)))

[Cameron Torrance]

I wasn't aware of it but that fixed everything.

[Riccardo Brasca]

Are you aware of file#category_theory/limits/shapes/terminal?

[Riccardo Brasca]

We even already have docs#CommRing.punit_is_terminal

[Cameron Torrance]

I was maybe a bit quick say it fixed everything, I now need assumptions like final_ring.{u u} Z ∧ final_ring.{u v} Z. I don't really see any way around this unless you could return things like forall universes , blah.

[Yaël Dillies]

You can. That's what universes is for.

[Yaël Dillies]

Do you know you can use(max u v) to mean "Any universe bigger than u"?

[Cameron Torrance]

Riccardo Brasca said:

Are you aware of file#category_theory/limits/shapes/terminal?

It seems they are fixing a universe level for the objects which I'm definitely coming to believe is a sensible thing to do.

[Cameron Torrance]

Yaël Dillies said:

You can. That's what universes is for.

Can you return functions that take universes as arguments? My vague impression was that this is impossible.

[Yaël Dillies]

No, but I don't really undersstand what your problem is, to be fair.

[Reid Barton]

Yeah, there's no way to say that a variable ring Z is final in every universe at once, as a hypothesis.

[Cameron Torrance]

Is better to fix a universe or to carry around morally redundant hypothesis? I would less worried if universes were cumulative, is there natural way of coercing types in one universe into types in a higher universe? .

[Reid Barton]

There is, docs#ulift

[Cameron Torrance]

thanks