When do universes higher than Type 0 become usefull?

Stream: new members

[Johannes C. Mayer]

I was wondering when you would use the type universes in LEAN, that are above Type 0. It seems that normally the return type of a function would be something like this:

universes u v

def uni (α : Type u) (β : Type v) (a : α) (b : β) : Type (imax u v) :=
sorry

So if you only have definitions that look like this, and you only ever use types that are in Type 0, then you would never get any term of type higher than Type 0. So is having these universes just a way to avoid Girad's paradox (I don't really get the paradox though). Or is there some practical relevance, in the sense that you can do something with the type universes. Or would you basically just ignore them usually.

[Eric Rodriguez]

I'm not sure it'll help much in your understanding of girard's paradox, but here's a thread about it and here is the mathlib formalization.

Furthermore, I think in LTE there's things in Type 1 and maybe even Type 2 (see condensed/Ab.lean, there they consider a topological commutative additive group living in Type 1 or above) just naturally, stemming from the idea that the set of all sets isn't a set, but sometimes we want to consider these sorts of things in category theory (c.f. locally small categories and so on); I think Kevin was talking yesterday about how Lean is slightly weaker than some axioms usually used for algebraic geometry (grothendieck-universe related).

[Kevin Buzzard]

For standard undergraduate mathematics you can just use Type, and indeed when teaching I do typically just use Type. My mental model of things is that Type 1 and higher are only there because one of the rules of type theory is that everything has to have a type, so Type has to have a type and there you go.

[Johannes C. Mayer]

Ok, so I updated towards that types that live in universes above Type 0 are probably useful sometimes, but that you don't need it most of the time.

[Kevin Buzzard]

For thousands of years mathematicians got by without categories, but now we use them a lot, and many categories are too large to be sets (e.g. the category of all sets isn't a set, and this corresponds to the fact that the category of all types does't live in Type in Lean). So if you want to do categories then universes suddenly become much more important.

[Kyle Miller]

A natural way the higher type universes appears is if you work with an indexed family of types (α : I → Type with I : Type) then α is a Type 1. A family of elements of this is a function x : Π (i : I), α i, and Π (i : I), α i is just a Type though.

You can get around Type 1 by deciding your indexed family of types can all be regarded as being subsets of some fixed type (have α : I → set β for some β : Type), since then α is a Type rather than a Type 1. You can still form Π (i : I), α i, where α i is using the implicit coercion from set to subtype, and this function type is still in Type.

[Kyle Miller]

One place indexed families show up is in recursors, like nat.rec. If you specialize the motive of nat.rec to be an indexed family of Types, then nat.rec is a Type 1, though as soon as you give it the motive argument it's back to being a Type.

[Sebastian Reichelt]

Here is a beginner-friendly special case. Consider a structure like:

structure group :=
(α : Type)
(e : α)
...

Then group has type Type 1.
(While this matches the standard way of defining a group in mathematics, it's not the standard way in Lean though.)

[Kevin Buzzard]

That is essentially the way the category docs#Group of groups is defined though. Except they allow \alpha : Type u so the category ends up having type Type u+1

[Yaël Dillies]

Kyle Miller said:

A natural way the higher type universes appears is if you work with an indexed family of types (α : I → Type with I : Type) then α is a Type 1. A family of elements of this is a function x : Π (i : I), α i, and Π (i : I), α i is just a Type though.

I'm confused by this example. Aren't α and Π (i : I), α i "the same type"?

[Yakov Pechersky]

Only up to funext, no?

[Yaël Dillies]

Yes, but how come that change the universe it lives in?

[Kyle Miller]

@Yaël Dillies In normal math notation, α is giving an $I$-indexed family of sets $(X_i)_{i\in I}$, and a term x : Π (i : I), α i is regarded as an $I$-indexed family of elements $(x_i)_{i\in I}$ with $x_i\in X_i$ for all $i\in I$.

[Kyle Miller]

I usually have to think through how it's α : Π (i : I), Type versus x : Π (i : I), α i.

[Yaël Dillies]

I didn't mean x : Π (i : I), α i, but Π (i : I), α i itself. (Π (i : I), α i) i and α i are "equal" for all i, so why aren't Π (i : I), α i and α "equal"?

[Kyle Miller]

@Sebastian Reichelt Interestingly, even if you do

structure group (α : Type) :=
(e : α)
...

then group is a function Type -> Type, which is a Type 1. If you want to prove things about type constructors like group, then it's nice having these higher type universes. (A Haskeller-friendly example is the monad typeclass, which requires having an argument from a higher universe.)

[Reid Barton]

Pi is not lambda

[Kyle Miller]

@Yaël Dillies Oh, I see, I think my brain tried to correct the types without me noticing (since α is a function so isn't a type). In the dependent type theory Lean uses, pi types and functions are considered to be different -- I don't really understand exactly why.

In Automath, pis are encoded as lambdas, and there's some rule that says lambdas may be regarded as types.

[Yaël Dillies]

Ah so they are morally equal but not Lean-equal? I guess that's an answer.

[Reid Barton]

I think it's more like they are morally different but it is possible to treat them as the same--I've heard about this before, but it seems deeply weird to me

[Reid Barton]

One is a family of sets, the other is the cartesian product of that family, which is another set

[Kyle Miller]

@Yaël Dillies I think the universe levels still sort of work out. We have that α : Π (i : I), Type : Type 1 and Π (i : I), α i : Type : Type 1, right? So α "as a type" is inside Type.

[Eric Rodriguez]

huh, they don't even live in the same universe:

universes u v

variables {ι : Type u} {α : ι → Type v}

example : (Π i, α i) == α := sorry --universe error

[Yaël Dillies]

Hmm

[Kyle Miller]

(deleted)

[Eric Rodriguez]

What do you mean? I see a very specific issue for, say, u=7 v=2.

[Kyle Miller]

Oh, I meant for just the u=0, v=0 case. Edit: actually, heq is ok here; need to work on my intuition here it seems (and heq is for things that agree at two levels up).

[Kyle Miller]

It turns out you can make a has_coe_to_sort to sort of add a rule that lambdas can be used as pi types:

universes u v

instance {α : Type u} :
  has_coe_to_sort (α → Type v) (Type (max u v)) :=
⟨λ f, Π (i : α), f i⟩

-- the family of types for vectors of various lengths
def α : ℕ → Type := λ n, vector ℤ n

-- the family of elements of those types of constant-0 vectors
def x : α := λ n, vector.repeat 0 n

@Yaël Dillies: and there's a "proof" that Π (i : I), α i and α are the same:

example {I : Type u} {α : I → Type v} :
  (Π (i : I), α i) = α :=
rfl

("proof" is in quotes because this is just the definition of the coercion.)

[Yaël Dillies]

Interesting!

[Kyle Miller]

It's curious how with {ι : Type u} {α : ι → Type v},

Π (i : ι), α i : Type (max u v) : Type (max (u+1) (v+1))

but

α              : ι → Type v     : Type (max u (v+1))

The universes Type (max (u+1) (v+1)) and Type (max u (v+1)) coincide when u <= v, but when α is indexing with "too big" of a type, then the pi type is in a sense in a bigger universe than α. Why is this?

[Eric Rodriguez]

Yes, this was the thing that was so mysterious to me.

[Eric Rodriguez]

I was going to say morally α can't be injective if the index set is too big but knowing set theory it's probably independent

[Yaël Dillies]

ι being in a big universe doesn't mean it's big, right? After all we can always ulift anything we want.

[Eric Rodriguez]

OK, but let's say that α isn't small for any universe less than it's in, then