Universe inequalities

Stream: mathlib4

[Scott Morrison]

Johan and I have been experimenting with a typeclass to represent universe inequalities. (With a critical clue from Reid.)

The main (only?) place we need universe inequalities in mathlib is in constructing (co)limits in the category of types (or other concrete categories). If we have a Type u indexed family in Type v, then the product (or more generally the subtype of the product giving a limit) will be in Type max u v. However we want this to live in Type v.

The proposal is very simple:

abbrev UnivLE.{u, v} : Prop := ∀ α : Type max u v, Small.{v} α

example : UnivLE.{u, u} := inferInstance
example : UnivLE.{u, u+1} := inferInstance
example : UnivLE.{0, u} := inferInstance
example : UnivLE.{u, max u v} := inferInstance

Note that this is not the immediately obvious definition, which would be ∀ α : Type u, Small.{v} α. This is weaker, and implied by the definition above. We need this stronger definition precisely for the construction of limits discussed above.

This definition does have some defects, in particular not being transitive in Lean's type theory, but so far this doesn't seem to be a practical obstacle.

• branch#UnivLE gives the basic definitions

• branch#UnivLE_types uses this definition to construct the appropriate HasLimitsOfSize instance, depending on a UnivLE hypothesis.

With this design all of the following work:

example : HasLimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (Type max v w) := inferInstance
example : HasLimitsOfSize.{0, 0, v, v+1} (Type v) := inferInstance
example : HasLimitsOfSize.{v, v, v, v+1} (Type v) := inferInstance
example [UnivLE.{v, u}] : HasLimitsOfSize.{v, v, u, u+1} (Type u) := inferInstance

• branch#UnivLE_UniqueGluing then explores how we might do the universe generalisations from !3#19153 (since reverted in !3#19230) but using UnivLE typeclasses instead of max u v universes.

[Scott Morrison]

Unless I hear screams of anguish, I will convert these branches into PRs soon.

[Yury G. Kudryashov]

Am I right that it is not transitive because nothing in the specification says that max u v is actually u or v?

[Yury G. Kudryashov]

And it becomes transitive if we add an axiom ∀ α : Type max u v, Small.{u} α ∨ Small.{v} α?

[Matthew Ballard]

TypeMax will be phased out with UnivLE phasing in, right? How does eg commutativity of limits look? That’s the most basic situation for chaining things that I can think of.

[Scott Morrison]

I hope we can phase out TypeMax in favour of UnivLE. I haven't looked at commutativity of limits yet. If you have a suggestion about which files to look at, I can try that.

(Although I'd prefer not to put much more work into UnivLE in the near future if possible. If anyone else wants to try this that would be great.)

[Scott Morrison]

@Yury G. Kudryashov, yes, nothing says max u v is actually u or v. In fact I think there's not even any sense in which is the smallest thing bigger than both u and v. (i.e. not only are universe not linearly ordered, max is not even a least upper bound).

[Matthew Ballard]

I should have led with: I think this is a definite all around improvement and thanks for doing it!

[Gabriel Ebner]

I think this should be a def instead of an abbrev though.

[Johan Commelin]

Concerning transitivity: if/when we need this, we can just add the transitive inequality as an extra assumption. TC will be able to find it in concrete situations via other instances. In theory, this could lead to a blow up of assumption, but in practice I think we are quite far removed from such problems. If it ever becomes a problem, we'll cross that bridge when we get to it.

[Scott Morrison]

These are now PRs at #5723, #5724, and #5726.

[Scott Morrison]

@Gabriel Ebner, could you say why it should be a def (presumably actually a class)?

I would need to convert the examples in #5723 into actual instances.

[Gabriel Ebner]

Ah I didn't realize that this is a class, then it's not so bad. In general it's problematic for simp to have abbreviations that are more complex than abbrev ge (x y : α) := y ≤ x.

import Mathlib.CategoryTheory.UnivLE
example (h : UnivLE.{u,v}) : UnivLE.{u,v} := by
  simp [h] -- unsolved goals

[Gabriel Ebner]

This is because simp will see through the abbreviation when looking at the hypothesis (i.e., it gets Small.{v} ?α) but then won't find it when simplifying UnivLE.{u,v}.

[Johan Commelin]

I really look forward to having the option to say: this ring lives in a universe that is smaller than this module.

[Scott Morrison]

I think it would be okay to turn it into a one-field class, and writing a single instance going from the current definition to UnivLE (taking advantage of loops being allowed!) But I think I'd prefer to wait to see if that is useful later.

[Scott Morrison]

If someone would like to investigate UnivLE.{u+1, u} → False, that might be fun. Can this be derived from Girard's paradox?

[Kyle Miller]

It's true, thanks to @Chris Hughes (zulip)

attribute [mk_iff] Small

example : ¬ UnivLE.{u+1, u} := by
  unfold UnivLE
  simp [Small_iff]
  use Type u
  intro α
  constructor
  intro f
  exact Function.not_surjective_Type.{u, u} f.symm f.symm.surjective

[Scott Morrison]

Thanks @Kyle Miller, PR'd as #5739.

[Scott Morrison]

On the next UnivLE PR #5724, I have the following alarming situation:

#synth X   -- succeeds!
example : X := inferInstance   -- fails!

where the failure is:

stuck at solving universe constraint
  v₁ =?= max v₁ ?u.33468
while trying to unify
  UnivLE.{v₁, v₁}
with
  (α : Type v₁) → (∀ (α : Type v₁), Small.{max ?u.33468 v₁, v₁} α) α

[Scott Morrison]

More specifically this is:

#synth HasProducts.{v₁} (Type v₁)  -- Succeeds!
example : HasProducts.{v₁} (Type v₁) := inferInstance  -- Fails!

in the file Mathlib/CategoryTheory/Closed/Types.lean.

[Scott Morrison]

It's not a show-stopper, as I can provide a shortcut for the instance as

instance : HasProducts.{v₁} (Type v₁) := fun _ ↦ hasLimitsOfShapeOfHasLimits.{v₁, v₁, v₁, v₁ + 1}

and then proceed.

[Scott Morrison]

But it feels like #synth succeeding and inferInstance failing might count as a bug?

@Gabriel Ebner, do you know an explanation for why they might diverge?

[Yury G. Kudryashov]

What if you add a shortcut instance for Small?

[Gabriel Ebner]

I guess this happens because UnivLE is unfolded somewhere (it's an abbrev after all) and we then unify Small.{max ...} with Small.{max ...}. Can you try changing UnivLE to a class?

[Scott Morrison]

I did try changing it to a class, and it is just failure all down the line! I couldn't even get the instance [UnivLE.{u, v}] (α : Type u) : Small.{v} α := example to compile, no matter how many universe annotations I added. I had to actually pass the UnivLE.small instances in by hand.

[Scott Morrison]

That is, where we currently have:

abbrev UnivLE.{u, v} : Prop := ∀ α : Type max u v, Small.{v} α

pp_with_univ UnivLE

example : UnivLE.{u, u} := inferInstance
example : UnivLE.{u, u+1} := inferInstance
example : UnivLE.{0, u} := inferInstance
example : UnivLE.{u, max u v} := inferInstance

instance [UnivLE.{u, v}] (α : Type u) : Small.{v} α :=
  ⟨Shrink.{v, max u v} (ULift.{v} α),
    ⟨Equiv.ulift.symm.trans (equivShrink (ULift α))⟩⟩

the best I could mange with UnivLE a class was:

class UnivLE.{u, v} : Prop where
  small : ∀ α : Type max u v, Small.{v} α

attribute [instance] UnivLE.small

pp_with_univ UnivLE

instance : UnivLE.{u, u} := ⟨inferInstance⟩
instance : UnivLE.{u, u+1} := ⟨inferInstance⟩
instance : UnivLE.{0, u} := ⟨inferInstance⟩
instance : UnivLE.{u, max u v} := ⟨inferInstance⟩

instance [I : UnivLE.{u, v}] (α : Type u) : Small.{v} α :=
  ⟨@Shrink (ULift.{v} α) (I.small _),
    ⟨Equiv.ulift.symm.trans (@equivShrink (ULift α) (UnivLE.small _))⟩⟩

[Matthew Ballard]

SmallMax?