# Zulip Chat Archive

## Stream: new members

### Topic: universe levels

#### Fabian Glöckle (Apr 01 2019 at 16:01):

Hello, can you help me understanding universe levels?

I am working on the lemma

lemma dual_dim_eq [fintype B] : dim K V = dim K (dual K V) :=

(`B`

being a basis of the finite dimensional `K`

-vectorspace `V`

)

which produces the error

type mismatch at application dim K (dual K V) term dual K V has type Type (max u_2 u_1) : Type (max (u_2+1) (u_1+1)) but is expected to have type Type u_2 : Type (u_2+1)

The problem is that `dual := V →ₗ[K] K`

produces a type necessarily over the universe levels of `K`

and `V`

, whereas `vector_space.dim`

works with a universe level of the vector space which is independent of the one of `K`

.

How does Lean deal with such situations?

And can I read up on universe levels anywhere more thoroughly?

#### Kevin Buzzard (Apr 01 2019 at 16:06):

I'm not sure this should be happening. Hmm.

#### Kevin Buzzard (Apr 01 2019 at 16:07):

Can you post a minimum working example -- something which compiles and which I can just cut and paste? All imports included etc.

#### Fabian Glöckle (Apr 01 2019 at 16:08):

Is there a coercion to higher universe levels? If I change the two sides of the equality statement of the lemma, I get

type mismatch at application dim K V term V has type Type u_2 : Type (u_2+1) but is expected to have type Type (max u_2 u_1) : Type ((max u_2 u_1)+1)

#### Kevin Buzzard (Apr 01 2019 at 16:08):

Can you point me to the definition of `dim`

?

#### Fabian Glöckle (Apr 01 2019 at 16:09):

`vector_space.dim`

in `linear_algebra.dimension`

#### Kevin Buzzard (Apr 01 2019 at 16:10):

dim : Π (α : Type u_1) (β : Type u_2) [_inst_1 : discrete_field α] [_inst_2 : add_comm_group β] [_inst_3 : vector_space α β], cardinal

This looks fine to me -- there's no reason K and V have to be in the same universe.

#### Kevin Buzzard (Apr 01 2019 at 16:11):

The issue is I guess the cardinals being in different universes.

#### Reid Barton (Apr 01 2019 at 16:12):

You could use `cardinal.lift`

#### Kevin Buzzard (Apr 01 2019 at 16:12):

Or you could turn the cardinal into a natural number before you ask about the equality.

#### Kevin Buzzard (Apr 01 2019 at 16:12):

I've never used cardinals in Lean, I am not much help.

#### Fabian Glöckle (Apr 01 2019 at 16:18):

The cardinal lift was what I was looking for (I did not know they depended on universes, but of course that makes much sense). Thank you all for the quick help!

#### Kenny Lau (Jul 12 2019 at 06:45):

structure B := (C : Type u) #check B.{u} -- B : Type (u+1)

#### Kenny Lau (Jul 12 2019 at 06:46):

Why isn't it `B : Type u`

?

#### Ken Lee (Jul 12 2019 at 06:50):

what does the projection looking '.{u}' mean?

#### Kenny Lau (Jul 12 2019 at 06:51):

it's specifying the universe parameters

#### Ken Lee (Jul 12 2019 at 06:54):

Uh... so the universe that C is supposed to be in?

#### Kenny Lau (Jul 12 2019 at 07:01):

right

#### Chris Hughes (Jul 12 2019 at 07:09):

This is why.

import set_theory.schroeder_bernstein universe u structure B := (C : Type u) lemma eq.mpr_injective {α β : Sort u} (h : α = β) : function.injective (eq.mpr h) := λ _ _, by cases h; exact id instance : inhabited B := ⟨⟨pempty⟩⟩ open function example {α : Type u} (f : B.{u} ↪ α) : false := let g := B.C ∘ inv_fun f in have hg : surjective g, from surjective_comp (λ x, ⟨B.mk x, rfl⟩) (inv_fun_surjective f.2), let X : Type u := sigma g in let a : α := classical.some (hg (X → Prop)) in have ha : g a = (X → Prop), from classical.some_spec (hg (set X)), cantor_injective (show set X → X, from λ s, ⟨a, by rw ha; exact s⟩) (λ x y h, by simp at *; exact eq.mpr_injective _ h)

#### Kenny Lau (Jul 12 2019 at 07:11):

thanks

#### Chris Hughes (Jul 12 2019 at 07:15):

You can prove the well ordering theorem using this idea, provided you already know cardinals are well ordered.

parameter {σ : Type u} open function noncomputable lemma embedding_to_cardinal : σ ↪ cardinal.{u} := classical.choice $ embedding.total.resolve_left $ λ ⟨⟨f, hf⟩⟩, let g : σ → cardinal.{u} := inv_fun f in let ⟨x, (hx : g x = 2 ^ sum g)⟩ := inv_fun_surjective hf (2 ^ sum g) in have g x ≤ sum g, from le_sum.{u u} g x, not_le_of_gt (by rw hx; exact cantor _) this /-- The relation whose existence is given by the well-ordering theorem -/ def well_ordering_rel : σ → σ → Prop := embedding_to_cardinal ⁻¹'o (<) instance well_ordering_rel.is_well_order : is_well_order σ well_ordering_rel := (order_embedding.preimage _ _).is_well_order

#### Bhavik Mehta (May 23 2020 at 23:31):

MWE:

```
import category_theory.comma
universes v u
namespace category_theory
open category_theory category_theory.category category_theory.limits
variables {C : Type u} [category.{v} C] {X : C}
structure sub' (X : C) :=
(arrow : over X)
[is_mono : mono arrow.hom]
instance mono_of_sub' (g : sub'.{v} X) : mono g.arrow.hom := g.is_mono
end category_theory
```

Any time I use `sub'`

I need to include the `{v}`

- is there any way around this? There was some recent fix which let me remove the `include`

stuff but I can't seem to find anything better here

#### Reid Barton (May 23 2020 at 23:36):

I've never really tried to figure out why sometimes Lean really wants the universe level--it seems correlated with the type of `sub'`

not mentioning morphisms, which makes sense of course. I've always sort of assumed Lean is correct here and it's not that much trouble to add the universe parameter...

#### Reid Barton (May 23 2020 at 23:36):

I think bundled categories would fix this.

#### Reid Barton (May 23 2020 at 23:37):

I think the behavior will change in Lean 4, too

#### Reid Barton (May 23 2020 at 23:38):

even though I think the Lean 3 behavior is technically correct

#### Reid Barton (May 23 2020 at 23:38):

Imagine you had a second `[category.{w} C]`

; would Lean know which instance to pick?

#### Bhavik Mehta (May 23 2020 at 23:39):

Fair enough - do you know why the recent fix lets us get rid of the `include`

stuff?

#### Reid Barton (May 23 2020 at 23:39):

Yes (since I wrote it :upside_down:)

#### Reid Barton (May 23 2020 at 23:39):

That was just a bug.

#### Reid Barton (May 23 2020 at 23:40):

It covered situations where Lean had already figured out it needed to use the `category.{v} C`

variable, but the universe parameter `v`

didn't otherwise appear anywhere

#### Reid Barton (May 23 2020 at 23:40):

in this case the elaborator would produce a bad declaration

#### Bhavik Mehta (May 23 2020 at 23:41):

Ah cool, I see. Can I remove the include everywhere in my code then?

#### Reid Barton (May 23 2020 at 23:41):

You might be wondering *why* Lean so frequently figures out to use the `category.{v} C`

instance (instead of holding out for a possibly different `category.{w} C`

instance) and this I don't know.

#### Reid Barton (May 23 2020 at 23:41):

Yes

#### Reid Barton (May 23 2020 at 23:41):

provided you also remove the instance name of course

#### Reid Barton (May 23 2020 at 23:41):

https://github.com/leanprover-community/mathlib/commit/cb3a017fa53baf886fca6f10e484b016264abd43

#### Reid Barton (May 23 2020 at 23:44):

I went through the library pretty quickly and skipped over some where I didn't understand immediately what was going on--those can probably be removed too.

#### Bhavik Mehta (May 23 2020 at 23:45):

I was just about to send an example where it didn't let me remove it, but in the process of minimising to an mwe I realised the file depended on another one which had an `include`

#### Reid Barton (May 23 2020 at 23:46):

hmm, I think these changes should not have any non-local effects...

#### Bhavik Mehta (May 23 2020 at 23:48):

Maybe I'd done something else wrong too then, in any case I've got something which seems to work now!

#### Mario Carneiro (May 24 2020 at 00:12):

My understanding is that typeclass inference is not "universe aware". Universe variables are always out params so a `category.{v} C`

and `category.{w} C`

instance would be considered conflicting. (I also think this is the correct behavior.)

#### Reid Barton (May 24 2020 at 00:16):

Well, that is what Lean 4 is supposed to implement

#### Reid Barton (May 24 2020 at 00:17):

In Lean 3 it doesn't always happen. I think it has something to do with the difference between regular and temporary metavariables

#### Reid Barton (May 24 2020 at 00:19):

By "it doesn't always happen" I mean Lean doesn't always use an instance if it would have to assign a universe level metavariable in the goal to do so.

Last updated: May 13 2021 at 17:42 UTC