Zulip Chat Archive

Stream: general

Topic: Universe issues


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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:28):

The error was

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:29):

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:30):

and this time I got

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

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:32):

Some experimentation led me to something which worked:

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:32):

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:32):

But this raises two questions for me:

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:33):

1) why wasn't I fine before?

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:33):

2) Will this fix cause me problems later?

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:34):

that is, U : beta -> set X

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:36):

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:36):

but that might be a bridge too far

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:36):

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:37):

what does that even mean

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:37):

foo is a thing

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:37):

and it has a type

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:37):

which lives in a universe

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:37):

it is universe polymorphic

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:38):

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:38):

foo' mentions a universe I don't even see

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:39):

or at least something mentions this universe

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:39):

foo and foo' are the same

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:39):

wait

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:39):

are they exactly the same?

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:39):

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:39):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:39):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:40):

yes. All universe polymorphic functions are like this

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:40):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:40):

exactly

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:40):

But where is this u_1 coming from?

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:40):

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:41):

gotcha

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:42):

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:42):

so why do I get a problem?

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:42):

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:43):

aah

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:43):

yes I just independently realised this

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:43):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:44):

it is

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

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:45):

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:46):

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

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:47):

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:47):

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

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:48):

I need to think about the last thing you said

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:49):

Thanks a lot for the fix and the advice though.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:51):

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

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:51):

hmm, I need to go and feed children

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:51):

thanks

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

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

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

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:14):

What is happening here:

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

-/

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

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:14):

oh

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:14):

heh

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:15):

ignore the irrelevant names

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:15):

If I change theorem to definition, it works

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:15):

And this works too:

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:16):

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

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

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:19):

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

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

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

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

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:28):

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

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:28):

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

view this post on Zulip Kevin Buzzard (May 22 2018 at 20:28):

and it wasn't Prop so Lean panicked

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

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

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