## 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 :=

#### 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