Questions about DTT

Stream: new members

[Bartosz Towiański]

Hi, I am learning the type theory that Lean is based on and have a couple of questions.

Why do we need an infinite number of type universes?
If #check Type instead yielded Type would this cause some paradox akin to Russell's?
Why does Sort u → Sort v have to live in the universe above, Type (max u v)? Is it arbitrary in the sense that any universe above both u and v works and this is just convention?

Why do the following dependent pair types not work?

universe u v
#check  (α : Sort u) → (β : α → Sort v) → Σ a : α, β a
#check  (α : Sort u) → (β : α → Type v) → Σ a : α, β a
#check  (α : Type u) → (β : α → Sort v) → Σ a : α, β a

Am I correct that the following syntaxes have been removed from Lean 4?

• Π a : α, β a
• constant, constants, variables, lemma

In mathlib, one sees ℕ, ℝ, ℂ written. Are there built-in aliases somewhere? They are not defined in my editor.

Thank you so much to whoever answers my questions!

[Riccardo Brasca]

Yes, Type : Type would give a proof of False. This quite subtle, it is proved in docs#Counterexample.girard

[Riccardo Brasca]

The problem is that we can not suppose Type : Type (Lean would say that this does not typecheck, so we can not even say that this implies False). What is done in docs#Counterexample.girard is essentially supposing that there exist Π and λ constructors that take values in Type, and derive a contradiction.

The proof is unfortunately very difficult to follow :sweat_smile:

[Yaël Dillies]

• As mathematicians, we don't. On paper, everything we do fits in Type 1. In Lean, for technical reasons, everything fits in Type 4 (or Type 5? don't remember). Metatheoretically however every type is supposed to have a type, so we need at least countably many universes
• Any higher universe will do
• Look at docs#PSigma
• Yes, although mathlib provides lemma back
• They are notations from mathlib

[Riccardo Brasca]

Concerning ℝ, note that you can ctrl-click in VS Code on the symbol, and it will bring you where it is defined. For example ℝ is defined here.

[Riccardo Brasca]

If you like Π, you can have

import Mathlib.Util.PiNotation
open scoped PiNotation

and the notation will work.

[Bartosz Towiański]

Wow, thank you so much for the quick responses! Yes, the Girard's paradox looks very gnarly indeed.

[Bartosz Towiański]

Riccardo Brasca said:

If you like Π, you can have

import Mathlib.Util.PiNotation
open scoped PiNotation

and the notation will work.

Ah yes, I was also wondering why Pi was removed but not Sigma, but looks like it's easy to get both anyway