Zulip Chat Archive

Stream: general

Topic: Type in type


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 04 2021 at 00:45):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Apr 04 2021 at 01:46):

And in contrast we have:

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 KUK\subseteq U from KUK\in U and hence UU is larger than KK. 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 05 2021 at 05:29):

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

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip David Wärn (Apr 05 2021 at 12:15):

#7042


Last updated: May 18 2021 at 17:44 UTC