## Stream: new members

### Topic: Type : Type

#### Mateusz Zugaj (Jun 04 2020 at 12:48):

What would happen if Type was of the type Type? I tried to make some sort of Russell's paradox out of this, but I cannot define a type T made of things that are not their own type.

#### Mateusz Zugaj (Jun 04 2020 at 12:49):

Sorry for a noob question

#### Jalex Stark (Jun 04 2020 at 12:52):

Which type are you talking about when you say Type? I think you mean Type u for some universe u

#### Jalex Stark (Jun 04 2020 at 12:53):

Type u has type Type (u +1)

#### Jalex Stark (Jun 04 2020 at 12:54):

When I type #check Type into VSCode it decides that I'm talking about Type 1

#### Reid Barton (Jun 04 2020 at 12:56):

If you use a recent enough Lean 3, I think the universe checks are disabled for meta inductive definitions, and then you can try to write your paradox.

#### Mateusz Zugaj (Jun 04 2020 at 12:56):

Yes, and I want to understand the need for "+1" in Type u : Type (u+1)

#### Mateusz Zugaj (Jun 04 2020 at 12:57):

Why there cannot be a type of all types?

#### Jalex Stark (Jun 04 2020 at 12:58):

are you asking a question about Lean's type theory or a question about type theories in general?

#### Reid Barton (Jun 04 2020 at 13:00):

meta inductive T : Type
| mk : Type → T


With a recent enough version, Lean will accept this and then you can implement the usual paradoxes.

#### Kevin Buzzard (Jun 04 2020 at 13:01):

What's the shortest meta proof of false?

#### Reid Barton (Jun 04 2020 at 13:03):

meta def a : false := a, but this isn't very exciting

#### Mateusz Zugaj (Jun 04 2020 at 13:33):

@Jalex Stark The question is about Lean's type theory, but I suppose the answer to the general question should be the same.

#### Jalex Stark (Jun 04 2020 at 13:35):

well, the answer for Lean's type theory is going to be something like "Lean requires the judgement relation : to be well-founded"
(with the caveat that I don't know whether the thing I'm saying is literally true. one can do real maths in Lean without understanding its type theory on a deep level)

#### Jalex Stark (Jun 04 2020 at 13:36):

whereas for general type theory it's going to be "well-founded judgement relations enjoy nice properties that ill-founded ones in general do not"

#### Reid Barton (Jun 04 2020 at 13:40):

I thought we had a proof in mathlib that Type (u+1) is bigger than Type u, but it's not easy to search for.

#### Mateusz Zugaj (Jun 04 2020 at 13:41):

@Jalex Stark "ill-founded ones in general do not" - so it's not like we have a paradox instantly, just some bad behaviour?

#### Reid Barton (Jun 04 2020 at 13:41):

No, there really is a paradox.

#### Jalex Stark (Jun 04 2020 at 13:42):

I was speaking mildly to avoid saying false things. Reid knows more than me and can speak more decisively.

#### Reid Barton (Jun 04 2020 at 13:48):

Although it's not super easy to see, it follows from https://github.com/leanprover-community/mathlib/blob/e397b4c/src/set_theory/ordinal.lean#L1855-L1868 that each universe has more ordinals than the previous one

#### Reid Barton (Jun 04 2020 at 13:55):

So, in Lean, you can prove not (Type u = Type (u+1)), and that should be pretty convincing that Type : Type would lead to inconsistency

#### Mateusz Zugaj (Jun 04 2020 at 14:12):

@Reid Barton Yes, that is convincing. The one more bit I'm missing is what exactly universes are, and why not u+1 = u. But that (I hope) I will learn from tutorials

#### Jalex Stark (Jun 04 2020 at 14:15):

i don't think the tutorials try to teach you that, since it's not very necessary for typical lean use cases

#### Reid Barton (Jun 04 2020 at 14:18):

I'm not sure what your background is, but for most people it's probably better to start out by taking on faith that Type : Type would lead to inconsistencies which are avoided by introducing universe levels.

#### Mateusz Zugaj (Jun 04 2020 at 14:23):

So one of my takeaways is that in ZFC it is really easy to say why the set of all sets doesn't exists, but it turns out that in type theory that it isn't so easy to say why there is not a type of all types, right?

#### Reid Barton (Jun 04 2020 at 14:34):

Yeah, somehow the global membership concept gives you easier access to these paradoxes. I guess another way to prove it in Lean should be to use its model of ZFC, and then run a proof that there is no set of all sets there.

#### Reid Barton (Jun 04 2020 at 14:37):

If you like ZFC then you may also want to think of the "intended model" of Lean as fixing a sequence $\mathcal{U}_0 \in \mathcal{U}_1 \in \cdots$ of Grothendieck universes, thinking of universe levels as external natural numbers $\{0, 1, \ldots\}$, and interpreting a type of type Type u as a set belonging to $\mathcal{U}_u$.

#### David Wärn (Jun 04 2020 at 15:00):

You should be able to derive a quick contradiction from Type : Type using Cantor?
Let K := Σ α : Type, α. Any α : Type injects into K. So assuming Type : Type, we get that set K embeds into K.

#### Kenny Lau (Jun 04 2020 at 15:09):

well Cantor's Theorem (or Russell's paradox) is that there is no surjection from A to P(A) right

#### Kenny Lau (Jun 04 2020 at 15:09):

but I guess you can noncomputably construct a surjection from an injection the other way

#### Chris Hughes (Jun 04 2020 at 15:24):

You can constructively prove there's no injection from the powerset.

how?

#### Jalex Stark (Jun 04 2020 at 15:45):

i think this is constructive:

given f : set \a \to \a,
make g (x : set \a) : \set \a := {a | \ex y \sub x, f y = a}

g has a least fixpoint x := \bigcup_n g^n \emptyset

f (g x) = f x \in x

since f x \in x, we must have f x \in g^n \emptyset for some finite n, contradicting injectivity

#### David Wärn (Jun 04 2020 at 16:02):

A formal proof:

import tactic

def K : Type 1 := Σ α : Type, α

def embed_sum (α : Type) : α → K := λ a, ⟨α, a⟩

lemma embed_inj (α : Type) : function.injective (embed_sum α) := by tidy

theorem cantor (α : Type) (f : set α → α)
(inj : function.injective f) : false :=
begin
let s := { x | ∃ t, f t = x ∧ ¬ x ∈ t },
have not_mem : ¬ f s ∈ s,
{ intro h,
suffices : ¬ f s ∈ s,
{ exact this h },
rcases h with ⟨t, ht, hn⟩,
rwa inj ht at hn, },
have is_mem : f s ∈ s := ⟨s, rfl, not_mem⟩,
exact not_mem is_mem,
end

-- fails due to some issue with universes...
-- theorem falso : false :=
-- cantor (set K) (embed_sum K) (embed_inj K)


#### Patrick Stevens (Jun 04 2020 at 16:40):

FWIW if you're interested in the general question of Type in Type, rather than how it applies to Lean, I found http://liamoc.net/posts/2015-09-10-girards-paradox.html very clear

#### Patrick Stevens (Jun 04 2020 at 16:41):

Although I can read Agda, so I can't promise it's readable to people who haven't spent ages learning the syntax of Agda :P

Last updated: May 14 2021 at 07:19 UTC