Stream: general

Topic: Universe issues

Kevin Buzzard (Apr 06 2018 at 19:28):

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 (Apr 06 2018 at 19:28):

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

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


The error was

Kevin Buzzard (Apr 06 2018 at 19:28):

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 (Apr 06 2018 at 19:29):

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

Kevin Buzzard (Apr 06 2018 at 19:30):

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
end


Kevin Buzzard (Apr 06 2018 at 19:30):

and this time I got

Kevin Buzzard (Apr 06 2018 at 19:30):

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 (Apr 06 2018 at 19:31):

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 (Apr 06 2018 at 19:31):

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

Kevin Buzzard (Apr 06 2018 at 19:32):

Some experimentation led me to something which worked:

Kevin Buzzard (Apr 06 2018 at 19:32):

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 (Apr 06 2018 at 19:32):

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

Kevin Buzzard (Apr 06 2018 at 19:32):

But this raises two questions for me:

Kevin Buzzard (Apr 06 2018 at 19:33):

1) why wasn't I fine before?

Kevin Buzzard (Apr 06 2018 at 19:33):

2) Will this fix cause me problems later?

Kevin Buzzard (Apr 06 2018 at 19:34):

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

Kevin Buzzard (Apr 06 2018 at 19:34):

that is, U : beta -> set X

Kevin Buzzard (Apr 06 2018 at 19:36):

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 (Apr 06 2018 at 19:36):

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

Kevin Buzzard (Apr 06 2018 at 19:36):

but that might be a bridge too far

Mario Carneiro (Apr 06 2018 at 19:36):

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

Kevin Buzzard (Apr 06 2018 at 19:37):

what does that even mean

foo is a thing

Kevin Buzzard (Apr 06 2018 at 19:37):

and it has a type

Kevin Buzzard (Apr 06 2018 at 19:37):

which lives in a universe

Mario Carneiro (Apr 06 2018 at 19:37):

it is universe polymorphic

Mario Carneiro (Apr 06 2018 at 19:38):

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

Mario Carneiro (Apr 06 2018 at 19:38):

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

Kevin Buzzard (Apr 06 2018 at 19:38):

foo' mentions a universe I don't even see

Kevin Buzzard (Apr 06 2018 at 19:39):

or at least something mentions this universe

Mario Carneiro (Apr 06 2018 at 19:39):

foo and foo' are the same

wait

Kevin Buzzard (Apr 06 2018 at 19:39):

are they exactly the same?

Mario Carneiro (Apr 06 2018 at 19:39):

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

Kevin Buzzard (Apr 06 2018 at 19:39):

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

Mario Carneiro (Apr 06 2018 at 19:39):

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

Mario Carneiro (Apr 06 2018 at 19:40):

yes. All universe polymorphic functions are like this

Kevin Buzzard (Apr 06 2018 at 19:40):

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

exactly

Kevin Buzzard (Apr 06 2018 at 19:40):

But where is this u_1 coming from?

Kevin Buzzard (Apr 06 2018 at 19:40):

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

Mario Carneiro (Apr 06 2018 at 19:41):

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

gotcha

Kevin Buzzard (Apr 06 2018 at 19:42):

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

Kevin Buzzard (Apr 06 2018 at 19:42):

so why do I get a problem?

Kevin Buzzard (Apr 06 2018 at 19:42):

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

Mario Carneiro (Apr 06 2018 at 19:42):

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

aah

Kevin Buzzard (Apr 06 2018 at 19:43):

yes I just independently realised this

Kevin Buzzard (Apr 06 2018 at 19:43):

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

it is

Mario Carneiro (Apr 06 2018 at 19:44):

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

Mario Carneiro (Apr 06 2018 at 19:45):

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

Mario Carneiro (Apr 06 2018 at 19:45):

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

Kevin Buzzard (Apr 06 2018 at 19:46):

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

Kevin Buzzard (Apr 06 2018 at 19:46):

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

Mario Carneiro (Apr 06 2018 at 19:47):

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

Kevin Buzzard (Apr 06 2018 at 19:47):

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 (Apr 06 2018 at 19:47):

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

Mario Carneiro (Apr 06 2018 at 19:48):

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 (Apr 06 2018 at 19:48):

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 (Apr 06 2018 at 19:48):

I need to think about the last thing you said

Mario Carneiro (Apr 06 2018 at 19:49):

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

Kevin Buzzard (Apr 06 2018 at 19:49):

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 (Apr 06 2018 at 19:49):

Thanks a lot for the fix and the advice though.

Kevin Buzzard (Apr 06 2018 at 19:51):

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

Kevin Buzzard (Apr 06 2018 at 19:51):

hmm, I need to go and feed children

thanks

Mario Carneiro (Apr 06 2018 at 19:54):

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 (Apr 06 2018 at 19:56):

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 (Apr 06 2018 at 19:56):

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

Kevin Buzzard (May 22 2018 at 20:14):

What is happening here:

Kevin Buzzard (May 22 2018 at 20:14):

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 (May 22 2018 at 20:14):

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

oh

heh

Kevin Buzzard (May 22 2018 at 20:15):

ignore the irrelevant names

Kevin Buzzard (May 22 2018 at 20:15):

If I change theorem to definition, it works

Kevin Buzzard (May 22 2018 at 20:15):

And this works too:

Kevin Buzzard (May 22 2018 at 20:16):

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


Kevin Buzzard (May 22 2018 at 20:16):

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

Kevin Buzzard (May 22 2018 at 20:19):

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


Kevin Buzzard (May 22 2018 at 20:19):

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 (May 22 2018 at 20:22):

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 (May 22 2018 at 20:28):

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

Kevin Buzzard (May 22 2018 at 20:28):

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

Kevin Buzzard (May 22 2018 at 20:28):

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

Kevin Buzzard (May 22 2018 at 20:28):

and it wasn't Prop so Lean panicked

Chris Hughes (Jun 01 2018 at 08:52):

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 (Jun 01 2018 at 09:01):

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 (Jun 01 2018 at 09:03):

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

Last updated: May 12 2021 at 03:23 UTC