## Stream: general

### Topic: Type in type

#### Kevin Buzzard (Apr 03 2021 at 23:34):

My son tells me that the type of type is type in python. I asked him if nat was equal to int in python and he said there wasn't a nat, but that int == string was false. I told him that if the type of type was type then he could probably prove that false was equal to true anyway. But I don't know the proof in lean. How do I prove false from Type : Type? This is Giraud's paradox right?

#### Mario Carneiro (Apr 03 2021 at 23:39):

Yes this is girard's paradox. It's a little hard to construct in lean because Type : Type doesn't typecheck

#### Mario Carneiro (Apr 03 2021 at 23:41):

I don't know any very easy proof. The usual proof is to construct something equivalent to ordinals and run the burali-forti paradox on the result

#### Mario Carneiro (Apr 03 2021 at 23:42):

I found http://www.cs.cmu.edu/~kw/research/hurkens95tlca.elf, although you have to read LF to follow it

#### Julian Berman (Apr 04 2021 at 00:14):

(Things in Python get quite fun when you also consider type is an instance (== term) and subclass of object, and object is an instance of type)

#### Julian Berman (Apr 04 2021 at 00:20):

If there were a nat in python though, it would not be equal to int. (E.g. there's a rational number type, and it's not equal to int.) In general the default in Python is objects compare for equality by identity by default, and it'd be silly to consider int and rational (or nat) equal to each other under the language semantics, there wouldn't be a reason to.

#### Julian Berman (Apr 04 2021 at 00:22):

We have an abstract base class (== gross version of a typeclass) that is the base of the number hierarchy: https://docs.python.org/3/library/numbers.html#numbers.Number -- so you are free to do class Natural(numbers.Number) if you truly felt like it.

#### Mario Carneiro (Apr 04 2021 at 00:44):

import data.set.basic

noncomputable theory
constant pi : (Type → Type) → Type
constant lam {A : Type → Type} : (∀ x, A x) → pi A
constant app {A} : pi A → ∀ x, A x
@[simp] axiom beta {A : Type → Type} (f : ∀ x, A x) (x) : app (lam f) x = f x

instance {A} : has_coe_to_fun (pi A) := ⟨_, app⟩

namespace girard

def univ : Type := pi (λ X, (set (set X) → X) → set (set X))

def τ (T : set (set univ)) : univ :=
lam $λ X f, {p | {x : univ | f (app x _ f) ∈ p} ∈ T} def σ (S : univ) : set (set univ) := app S _ τ @[simp] theorem τ_σ_def (s x) : s ∈ σ (τ x) ↔ {x : univ | τ (σ x) ∈ s} ∈ x := by simp [σ, τ] theorem paradox : false := begin let ω : univ := τ {p | ∀ x : univ, p ∈ σ x → x ∈ p}, let δ : set univ := {y | ¬ ∀ p : set univ, p ∈ σ y → τ (σ y) ∈ p}, have : ∀ p, (∀ x, p ∈ σ x → x ∈ p) → ω ∈ p, { refine λ p d, d ω _, simp [ω], exact λ x h, d (τ (σ x)) (by simpa) }, refine this δ (λ x e f, f δ e (λ p h, _)) (λ p h, _), { exact f {y | τ (σ y) ∈ p} (by rwa [τ_σ_def] at h) }, { exact this {y | τ (σ y) ∈ p} (by simpa [ω] using h) } end end girard  #### Mario Carneiro (Apr 04 2021 at 00:45): I can't honestly say I understand the proof, but it typechecks #### Bhavik Mehta (Apr 04 2021 at 01:45): Here's one way you can do this in Lean without new constants: We can show that Type isn't small, ie it's not possible for a type to be equivalent to Type: import logic.small lemma cast_helper {A : Type → Type} (x y : Type) (f : Π (x : Type), A x) (yx : y = x) : cast (congr_arg A yx) (f y) = f x := begin subst yx, simp, end theorem no_type_in_type : ¬ small.{0} Type := begin introI h, let pi : (Type → Type) → Type := λ f, Π (y : shrink Type), f ((equiv_shrink Type).symm y), let lam : Π {A : Type → Type}, (∀ x, A x) → pi A := λ A p t, p _, let app : Π {A}, pi A → ∀ x, A x, { intros A p t, apply eq.mpr (congr_arg A _) (p (equiv_shrink Type t)), apply ((equiv_shrink Type).left_inv t).symm }, have beta : Π {A : Type → Type} (f : ∀ x, A x) (x), app (lam f) x = f x, { intros A f x, change cast _ (f _) = _, apply cast_helper, simp }, -- insert Mario's proof here end  From here the environment has the constants and axioms in Mario's proof and that should then go through #### Bhavik Mehta (Apr 04 2021 at 01:46): And in contrast we have: theorem type_in_type_one : small.{1} Type := small_self Type  #### Mario Carneiro (Apr 04 2021 at 01:49): I added this in #7026, using a structure for the axioms so that we don't have to add false axioms to mathlib #### Kevin Buzzard (Apr 04 2021 at 08:36): This is great -- thanks to both of you. I've seen Girard's paradox mentioned a few times but the references I've seen usually just mention that it's some kind of standard diagonal argument without giving further details. #### David Wärn (Apr 04 2021 at 10:04): Here's a simple (?) argument. Any α : Type embeds in the type K := Σ α : Type, α of pointed types via a => (_, a). This is injective by UIP. If Type itself is small, then so is K. So set K embeds in K, contradicting Cantor #### Mario Carneiro (Apr 05 2021 at 04:16): @David Wärn Actually I've been thinking about how to prove this by cantor for a while, it's surprisingly tricky. In particular, I don't think Girard follows directly from Cantor, and Bhavik's statement about smallness of Type might be provable by cantor but I haven't found a way yet. I don't think this proof works, because the assumptions aren't enough to know that K exists with the required properties. (It might be, if you actually change the type theory so that K : Type, but with only Bhavik's bijection assumption I don't think this is enough.) In particular, "If Type itself is small, then so is K" is intuitively obvious but has no easy proof #### Mario Carneiro (Apr 05 2021 at 04:22): In set theory, this is relatively straightforward, since the equivalent of Type will be a universe which is a superset of any of its members, so one can conclude $K\subseteq U$ from $K\in U$ and hence $U$ is larger than $K$. But type theory universes are not transitive sets, and so there might be only a few types that are themselves quite large. In lean, we know the set of types has to be at least as large as the set of all cardinals, which we know is large using some of Cantor's other observations, but I think a proof along these lines boils down to the burali-forti paradox so probably isn't any simpler than girard.paradox above #### Mario Carneiro (Apr 05 2021 at 04:39): actually, nevermind, that proof actually does go through theorem not_small_type : ¬ small.{u} (Type (max u v)) | ⟨⟨S, ⟨e⟩⟩⟩ := let K := Σ α : S, e.symm α in @function.cantor_injective K (λ a, ⟨e (set K), cast (e.3 _).symm a⟩) (λ a b e, (cast_inj _).1$ eq_of_heq (sigma.mk.inj e).2)


#### Greg Price (Apr 05 2021 at 05:09):

Very nice!

Golfed slightly from there, and with the last line made perhaps a bit clearer:

theorem not_small_type : ¬ small.{u} (Type (max u v))
| ⟨⟨S, ⟨e⟩⟩⟩ := let K := Σ α : S, e.symm α in
@function.cantor_injective K
(λ a, ⟨_, cast (e.left_inv _).symm a⟩)
(sigma_mk_injective.comp \$ (cast_bijective _).injective)


#### Greg Price (Apr 05 2021 at 05:28):

Or for such a nice proof, perhaps it's worth letting it stretch out a bit and giving a few more labels to things, in the interest of making it easy to see what's happening. Here's a version in that direction:

theorem not_small_type : ¬ small.{u} (Type (max u v)) :=
assume ⟨⟨(S : Type u), ⟨(repr : Type (max u v) ≃ S)⟩⟩⟩,
let K := Σ α : S, repr.symm α in
let sK := repr (set K) in
function.cantor_injective
(sigma.mk sK ∘ cast (repr.left_inv _).symm)
(sigma_mk_injective.comp (cast_bijective _).injective)


#### Mario Carneiro (Apr 05 2021 at 05:29):

There's another version of this on the Girard PR btw

#### David Wärn (Apr 05 2021 at 08:34):

Nice! Here's another version, using some lemmas not yet in small.lean

import logic.small
universe u

instance small.sigma {α : Type*} (β : α → Type*) [small.{u} α] [∀ a, small.{u} (β a)] :
small.{u} (Σ a, β a) :=
⟨⟨Σ a' : shrink α, shrink (β ((equiv_shrink α).symm a')),
⟨equiv.sigma_congr (equiv_shrink α) (λ a, by simpa using equiv_shrink (β a))⟩⟩⟩

instance small.set {α : Type*} [small.{u} α] : small.{u} (set α) :=
⟨⟨set (shrink α), ⟨equiv.set.congr (equiv_shrink α)⟩⟩⟩

theorem not_small_type : ¬ (small.{u} (Type u)) :=
by { introI, apply @function.cantor_injective (Σ α : Type u, α) (λ x, ⟨_, equiv_shrink _ x⟩),
intros a b h, simpa using h }


#### Bhavik Mehta (Apr 05 2021 at 11:11):

David Wärn said:

Nice! Here's another version, using some lemmas not yet in small.lean

import logic.small
universe u

instance small.sigma {α : Type*} (β : α → Type*) [small.{u} α] [∀ a, small.{u} (β a)] :
small.{u} (Σ a, β a) :=
⟨⟨Σ a' : shrink α, shrink (β ((equiv_shrink α).symm a')),
⟨equiv.sigma_congr (equiv_shrink α) (λ a, by simpa using equiv_shrink (β a))⟩⟩⟩

instance small.set {α : Type*} [small.{u} α] : small.{u} (set α) :=
⟨⟨set (shrink α), ⟨equiv.set.congr (equiv_shrink α)⟩⟩⟩

theorem not_small_type : ¬ (small.{u} (Type u)) :=
by { introI, apply @function.cantor_injective (Σ α : Type u, α) (λ x, ⟨_, equiv_shrink _ x⟩),
intros a b h, simpa using h }


If these first two aren't in small.lean I think they're worth a PR

#### David Wärn (Apr 05 2021 at 12:15):

#7042

Last updated: May 18 2021 at 17:44 UTC