Universe issues

Stream: general

[Kevin Buzzard]

I seem to not understand universes properly, or more precisely how to use them properly. I ran into the following issue with some code:

[Kevin Buzzard]

definition foo (X : Type*) := ∀ (β : Type*), true

theorem baz (X : Type*) (bar: foo X) (β : Type*) : true :=
begin
  have H := bar β, -- error
  admit,
end

[Kevin Buzzard]

The error was

[Kevin Buzzard]

type mismatch at application
  bar β
term
  β
has type
  Type u_3 : Type (u_3+1)
but is expected to have type
  Type u_2 : Type (u_2+1)
state:
X : Type u_1,
bar : foo X,
β : Type u_3
⊢ true

[Kevin Buzzard]

I figured I'd investigate more, so I next wrote this:

[Kevin Buzzard]

universes u v w x
set_option pp.universes true
definition foo' (X : Type u) := ∀ (β : Type v), true
theorem baz' (X : Type w) (bar' : foo' X) (β : Type x) : true :=
begin
  have H := bar' β, -- error
  admit,
end

[Kevin Buzzard]

and this time I got

[Kevin Buzzard]

type mismatch at application
  bar' β
term
  β
has type
  Type x : Type (x+1)
but is expected to have type
  Type u_1 : Type (u_1+1)
state:
X : Type w,
bar' : foo'.{w u_1} X,
β : Type x
⊢ true

[Kevin Buzzard]

This made me realise that I didn't understand what was going on, because there is still this universe u_1 mentioned, even though I thought I'd just explicitly written down what universe everything was in.

[Kevin Buzzard]

In particular, bar' seems to mention this universe u_1 and I'm not sure where this universe got involved.

[Kevin Buzzard]

Some experimentation led me to something which worked:

[Kevin Buzzard]

definition foo'' (X : Type u) := ∀ (β : Type u), true

theorem baz'' (X : Type v) (bar'' : foo'' X) (β : Type v) : true :=
begin
  have H := bar'' β, -- works
  exact H
end

[Kevin Buzzard]

i.e. "keep X and beta in the same universe and you'll be fine"

[Kevin Buzzard]

But this raises two questions for me:

[Kevin Buzzard]

1) why wasn't I fine before?

[Kevin Buzzard]

2) Will this fix cause me problems later?

[Kevin Buzzard]

In reality, X is a topological space and it is covered by open sets U i where each i has type beta

[Kevin Buzzard]

that is, U : beta -> set X

[Kevin Buzzard]

My instinct is always to just let everything live in different universes because who cares about universes anyway, that's the joy of type theory

[Kevin Buzzard]

In ZFC I would just let X and beta be in Type

[Kevin Buzzard]

but that might be a bridge too far

[Mario Carneiro]

When you defined foo, it had two universe parameters, corresponding to the two Type* instances

[Kevin Buzzard]

what does that even mean

[Kevin Buzzard]

foo is a thing

[Kevin Buzzard]

and it has a type

[Kevin Buzzard]

which lives in a universe

[Mario Carneiro]

it is universe polymorphic

[Mario Carneiro]

Think of it as being implicitly a forall over the universe variables

[Mario Carneiro]

except that lean has no universe variable binders, so it's all just free variables and substitution

[Kevin Buzzard]

foo' mentions a universe I don't even see

[Kevin Buzzard]

or at least something mentions this universe

[Mario Carneiro]

foo and foo' are the same

[Kevin Buzzard]

wait

[Kevin Buzzard]

are they exactly the same?

[Mario Carneiro]

except foo' is more explicit about the two universe variables, u and v

[Kevin Buzzard]

Should I think that foo' is really "for all universes u, ..."

[Mario Carneiro]

yes, they are exactly the same as far as lean is concerned

[Mario Carneiro]

yes. All universe polymorphic functions are like this

[Kevin Buzzard]

like when I make variables and then secretly I am writing "for all v..."

[Mario Carneiro]

exactly

[Kevin Buzzard]

But where is this u_1 coming from?

[Kevin Buzzard]

Didn't I name all my universes with foo'?

[Mario Carneiro]

foo' has two universe variables, named u and v in the definition, but since it's like a forall, whenever you use it these variables can be substituted for other things

[Kevin Buzzard]

gotcha

[Kevin Buzzard]

So foo' is for all universes u and v, [what I wrote]

[Kevin Buzzard]

so why do I get a problem?

[Kevin Buzzard]

why can't we just do universe unification or something?

[Mario Carneiro]

u_1 is the name of a universe variable in baz', since you reference foo' X which only fixes its first parameter by unification, lean invents a second variable u_1 so it becomes bar' : foo'.{w u_1} X

[Kevin Buzzard]

aah

[Kevin Buzzard]

yes I just independently realised this

[Kevin Buzzard]

But now bar' should be "for all universes u_1, ..."

[Mario Carneiro]

it is

[Mario Carneiro]

bar'.{w x u_1} has type forall (X : Type w) (bar' : foo'.{w u_1} X) (β : Type x), true

[Mario Carneiro]

And since u_1 and x are separate universe variables being generalized, inside the proof you can't assume they are equal

[Mario Carneiro]

so bar' β is a type error since bar' accepts a Type u_1

[Kevin Buzzard]

OK so you have convinced me that the underlying way that universes work mean that my initial attempts should not work.

[Kevin Buzzard]

So now the question is should I try to re-arrange things to make them work?

[Mario Carneiro]

just write foo'.{w x} instead of foo' in the type of bar'

[Kevin Buzzard]

Or should I go down the "might bite me later and I have no understanding as to whether it will" route of letting all universes be u

[Kevin Buzzard]

aah, oh great, so I can do what I want to do.

[Mario Carneiro]

In general, I try to avoid types with "internal universe variables" like foo' here, which has a forall whose universe is not constrained by the input parameters

[Kevin Buzzard]

definition  foo' (X : Type u) :=  ∀ (β : Type v), true

theorem  baz' (X : Type w) (β : Type x) (bar' : foo'.{w x} X) : true :=
begin
have H := bar' β, -- works :-)
exact H,
end

[Kevin Buzzard]

I need to think about the last thing you said

[Mario Carneiro]

that means to prefer def foo' (X : Type u) := ∀ (β : Type u), true over def foo' (X : Type u) := ∀ (β : Type v), true

[Kevin Buzzard]

because this is a massively minimised thing and in reality I will have to decide whether I can try to avoid the thing you want me to avoid

[Kevin Buzzard]

Thanks a lot for the fix and the advice though.

[Kevin Buzzard]

How do I know whether the thing you prefer will be safe for me?

[Kevin Buzzard]

hmm, I need to go and feed children

[Kevin Buzzard]

thanks

[Mario Carneiro]

It is slightly less universe parametric (it requires that two variables be the same), so you may need extra ulifts around, which may or may not be better than the often required .{w x} stuff that arises with this approach

[Mario Carneiro]

Generally you will have to be "universe conscious" when working with definitions with internal universe variables - lots of things will require annotation. cardinal, ordinal, and Set (the ZFC sets) are like this

[Mario Carneiro]

category may also be, this exact thing was a point of discussion with Scott a few weeks ago

[Kevin Buzzard]

What is happening here:

[Kevin Buzzard]

universe u

structure scheme :=
(β : Type u)

theorem scheme_of_affine_scheme (R : Type u) : scheme :=
{ β := R -- universe issue
}

/-

type mismatch at field 'β'
  R
has type
  Type u : Type (u+1)
but is expected to have type
  Type u_1 : Type (u_1+1)

-/

[Kevin Buzzard]

Seems to me that scheme has decided that it wants to live in a different universe to beta and R

[Kevin Buzzard]

oh

[Kevin Buzzard]

heh

[Kevin Buzzard]

ignore the irrelevant names

[Kevin Buzzard]

If I change theorem to definition, it works

[Kevin Buzzard]

And this works too:

[Kevin Buzzard]

theorem scheme_of_affine_scheme (R : Type u) : scheme.{u} :=
{ β := R -- works
}

[Kevin Buzzard]

OK so maybe the answer is simply "don't use theorem to define something which isn't a Prop"

[Kevin Buzzard]

definition scheme_of_affine_scheme (R : Type u) : scheme :=
{ β := R -- works
}

[Kevin Buzzard]

I guess I don't understand what's going on, but on the other hand I can see I was doing something dumb.

[Chris Hughes]

This gives some small insight.

set_option pp.universes true
def scheme_of_affine_scheme (R : Type u) : scheme :=
begin
-- R : Type u
-- ⊢ scheme.{?l_1}
end

lemma scheme_of_affine_scheme (R : Type u) : scheme :=
begin
-- R : Type u
-- ⊢ scheme.{u_1}
end

[Kevin Buzzard]

Aah so in the first case scheme is in some universe and Lean isn't too fussed, it will decide later

[Kevin Buzzard]

but in the second case Lean decided to go for it and make a decision

[Kevin Buzzard]

because it's a lemma so the universe is supposed to be Prop

[Kevin Buzzard]

and it wasn't Prop so Lean panicked

[Chris Hughes]

The lemma card_univ below does not work without the .{u} in the fintype instance

import data.set.finite
open set fintype
universe u

def equiv_univ (α : Type u) : α ≃ (set.univ : set α) :=
{ to_fun := λ a, ⟨a, mem_univ _⟩,
  inv_fun := λ a, a.1,
  left_inv := λ a, rfl,
  right_inv := λ ⟨a, ha⟩, rfl }

@[simp] lemma card_univ {α : Type u} [fintype α] [fintype.{u} (set.univ : set α)]:
  @fintype.card (set.univ : set α) _ = fintype.card α :=
eq.symm (@card_congr α (set.univ : set α) _ _ (equiv_univ α))

The following do not work.

set_option pp.universes true
@[simp] lemma card_univ {α : Type u} [fintype α] [fintype (set.univ : set α)]:
  fintype.card (set.univ : set α) = fintype.card α :=
eq.symm (card_congr (equiv_univ α))

Gives the error

failed to synthesize type class instance for
α : Type u,
_inst_1 : fintype.{u} α,
_inst_2 : fintype.{?l_1} ↥univ.{u}
⊢ fintype.{u} ↥univ.{u}

and

set_option pp.universes true
@[simp] lemma card_univ {α : Type u} [fintype α] [f : fintype (set.univ : set α)]:
  @fintype.card (set.univ : set α) f = fintype.card α :=
eq.symm (@card_congr α (set.univ : set α) _ f (equiv_univ α))

Gives the error

type mismatch at application
  card_congr.{u u_1} (equiv_univ.{u} α)
term
  equiv_univ.{u} α
has type
  equiv.{u+1 (max 1 (u+1))} α
    (@coe_sort.{(max (u+1) 1) (max 1 (u+1))+1} (set.{u} α) (@set.has_coe_to_sort.{u} α) (@set.univ.{u} α)) : Type u
but is expected to have type
  equiv.{u+1 u_1+1} α
    (@coe_sort.{(max (u+1) 1) (max 1 (u+1))+1} (set.{u} α) (@set.has_coe_to_sort.{u} α)
       (@set.univ.{u} α)) : Type (max (max u u_1) u_1 u)

What's going on here? And will the .{u} in the fintype instance make the lemma more difficult to use. It worked in my application, but will it always work?

[Gabriel Ebner]

And will the .{u} in the fintype instance make the lemma more difficult to use.

No, not at all. It is the only possible choice, the elaborator just can't figure it out for whatever reason.

[Gabriel Ebner]

(The universe parameter .{u} is always there, whether you write it explicitly or not.)