Type in type

Stream: general

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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

[Julian Berman]

(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]

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]

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]

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]

I can't honestly say I understand the proof, but it typechecks

[Bhavik Mehta]

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]

And in contrast we have:

theorem type_in_type_one : small.{1} Type := small_self Type

[Mario Carneiro]

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]

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]

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]

@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]

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]

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]

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]

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]

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

[David Wärn]

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]

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]

#7042