Type 0 contains a universe

Stream: maths

[Kenny Lau]

What’s the simplest way to state the proposition that Type 0 contains a universe?

[Aaron Liu]

What does that mean?

[Aaron Liu]

I guess you could state that it forms an inaccessible cardinal

[Kenny Lau]

yeah probably

[Matt Diamond]

is it possible to prove that the cardinality of Type 0 is inaccessible? the cardinality of Type u is notoriously hard to pin down... in fact I think the exact value may be independent of Lean

you can certainly prove that the cardinality of Type u is greater than or equal to an inaccessible cardinal (specifically Cardinal.univ.{u, u+1})... maybe that's good enough

[Matt Diamond]

oh wait, you were just asking about stating it, not proving it... nvm

[Kenny Lau]

I'm just wondering if there's a convenient way to state it in terms of type theory and basically without much reference to cardinality

[Matt Diamond]

I guess I'm not sure what you specifically mean by "universe"

[Kenny Lau]

let's say it's equivalent to |X| being an inaccessible cardinal

[Matt Diamond]

well, by that definition, Cardinal would be a universe, as would Ordinal

[Kenny Lau]

The only problem is that they don't live in Type 0

[Kenny Lau]

in fact you can't actually prove what i asked

[Matt Diamond]

hmm

[Matt Diamond]

wait, so is the answer to your question just ∃ (α : Type 0), (#α).IsInaccessible?

[Kenny Lau]

yes, but I'm wondering if there's a more "accessible" (lol) way to write that

[Matt Diamond]

gotcha

[Kenny Lau]

For example, consider the following attempt:

Partial example

import Mathlib

universe u

-- https://en.wikipedia.org/wiki/Grothendieck_universe
def IsUniverse (α : Type u) : Prop :=
  ∃ (f : α → Type u), -- Every element can be realised as a type.
  (∀ x, ∃ y, Nonempty (Set (f x) ≃ f y)) ∧ -- Powerset axiom.
  (∃ x, Nonempty (f x ≃ ℕ)) ∧ -- Infinity axiom.
  (∀ x, ∀ g : f x → α, ∃ y, Nonempty ((Σ i, f (g i)) ≃ f y)) -- Union axiom.

-- Might be a bit hard
theorem exists_universe_iff_exists_inaccessible :
    (∃ α, IsUniverse.{0} α) ↔ (∃ α : Cardinal.{0}, α.IsInaccessible) :=
  sorry

theorem isUniverseType0 : IsUniverse.{1} (Type 0) :=
  ⟨PLift,
  fun x ↦ ⟨Set x, sorry⟩,
  ⟨ℕ, ⟨Equiv.plift⟩⟩,
  fun x g ↦ ⟨(Σ i, g ⟨i⟩), sorry⟩⟩

[Kenny Lau]

hmm, this could be right! (i've edited it)

[Kenny Lau]

@Matt Diamond what do you think?

[Matt Diamond]

Looks plausible! (Though I'm not really the person to ask... my knowledge of this stuff doesn't go that deep.)

[Matt Diamond]

Might as well try to prove it, though!

[Kenny Lau]

I'll leave that to Mario :rofl:

[Matt Diamond]

lol good call

[Matt Diamond]

@Kenny Lau for the powerset axiom:

fun x ↦ ⟨Set x, by
  have h1 : PLift (Set x) ≃ Set x := Equiv.plift
  have h2 : Set (PLift x) ≃ Set x := ⟨
    fun s => PLift.down '' s,
    fun s => PLift.up '' s,
    fun _ => by simp [Set.image_image],
    fun _ => by simp [Set.image_image]
  ⟩
  exact ⟨h2.trans h1.symm⟩
⟩

[Kenny Lau]

Informal proof: recall that a strongly inaccessible cardinal is one that is uncountable, regular, and a strong limit cardinal.

• Uncountable: take the powerset of ℕ.
• Regular: this means its cofinality is itself, which is captured by the union axiom.
• Strong limit cardinal: That's the powerset axiom.

And for the other way round, note how I've used all three axioms in the above proof.

[Kenny Lau]

Actually I think I can do better, I can make it more usable by leaving Prop

[Matt Diamond]

do you mean defining Universe as a structure?

[Kenny Lau]

Attempt #2

import Mathlib

universe u

-- https://en.wikipedia.org/wiki/Grothendieck_universe
class Universe (α : Type u) : Type (u+1) where
  (obj : α → Type u)
  (set : α → α)
  (setEquiv : ∀ x, obj (set x) ≃ Set (obj x))
  (nat : α)
  (natEquiv : ℕ ≃ obj nat)
  (sigma : (x : α) → (g : obj x → α) → α)
  (sigmaEquiv : ∀ (x : α) (g : obj x → α), (Σ i, obj (g i)) ≃ obj (sigma x g))

-- Might be a bit hard
theorem exists_universe_iff_exists_inaccessible :
    (∃ α : Type 0, Nonempty (Universe.{0} α)) ↔ (∃ α : Cardinal.{0}, α.IsInaccessible) :=
  sorry

instance : Universe.{1} (Type 0) where
  obj := PLift
  set x := Set x
  nat := ℕ
  sigma _ g := Σ i, g ⟨i⟩
  setEquiv _ := Equiv.plift.trans (Equiv.Set.congr Equiv.plift.symm)
  natEquiv := Equiv.plift.symm
  sigmaEquiv _ _ :=
    Equiv.trans (Equiv.sigmaCongr Equiv.plift (fun _ ↦ Equiv.plift)) Equiv.plift.symm

[Kenny Lau]

The -> direction should be that you would consider the map from \a to Cardinal and then take the union.

The <- direction should be some sort of type-theoretic interpretation of V(\a) where V is the von Neumann universe

[Mario Carneiro]

Am I understanding correctly that you are trying to write down the thing that lean cannot prove (because Type universes are themselves inaccessible but do not necessarily contain inaccessibles)?

[Kenny Lau]

Mario Carneiro said:

Am I understanding correctly that you are trying to write down the thing that lean cannot prove

Correct.

[Mario Carneiro]

A popular way to write this in type theory is to use inductive-recursive types

[Kenny Lau]

oh, that sounds fun, what does that mean?

[Mario Carneiro]

I'm not sure what the simplest inductive-recursive type that lean cannot prove (is equivalent to something that) exists is

[Mario Carneiro]

An inductive recursive type is when you define a function by recursion mutually with an inductive type

[Mario Carneiro]

it can be used to define models of type theory where you have an inductive type that produces codes for types mutually with a decoding function which turns the codes into actual types

[Kenny Lau]

Am I understanding correctly that you basically want to express the fact that an inaccessible cardinal is the a fixed point of beth that is also closed under union? And you want to use recursion to produce a fixed point of beth as well as make it closed under union?

[Kenny Lau]

I mean it also sounds like that since you said Lean cannot prove that it exists, then there's no way to actually write down the inductive type?

[Mario Carneiro]

in fact you kind of did this with your axiomatization, you are defining α by induction and obj : α → Type u by recursion, mutually

[Kenny Lau]

I see

[Mario Carneiro]

You can write down some syntax that would plausibly produce the object, except that lean doesn't support inductive recursive types

[Mario Carneiro]

Agda does, so people use this trick a lot over there

[Kenny Lau]

and reasonably so, because otherwise you would break Godel?

[Mario Carneiro]

no

[Mario Carneiro]

it's just an incredibly strong assumption

[Mario Carneiro]

models of type theory that support I-R types need Mahlo cardinals, not just inaccessibles

[Kenny Lau]

I see, so basically Agda could prove that Type contains a "universe", but that universe wouldn't be closed under I-R types?

[Mario Carneiro]

right, you could prove the existence of a universe closed under lean style inductives but not I-R

[Kenny Lau]

interesting!

[Mario Carneiro]

(although I have to admit I hesitate to assert that because agda allows a lot of stuff)

[Kenny Lau]

so basically the entire "model" of Lean lives inside Agda's Type 0!

[Mario Carneiro]

well, actually it's more complicated than that, because Agda has predicative universes

[Mario Carneiro]

while Lean has impredicative Prop

[Mario Carneiro]

If agda is consistent, it is probably a subsystem of second order arithmetic

[Mario Carneiro]

but if you added an impredicative assumption like Prop ~= Bool then Agda would model all of lean comfortably within Type 0

[Aaron Liu]

Mario Carneiro said:

Agda does, so people use this trick a lot over there

wow I didn't know that

[Mario Carneiro]

I'm pretty sure "what kind of inductive types does agda support" is an open question

[James E Hanson]

Matt Diamond said:

in fact I think the exact value may be independent of Lean

Yes, it's definitely independent of Lean whether there's a set in Type 0 of inaccessible cardinality.

[James E Hanson]

But beyond that, even if every type in Type 0 is smaller than the first inaccessible cardinal $\kappa$, I would suspect that it's independent of Lean whether Type 0 itself has cardinality $\kappa$. Type theory is generally fairly agnostic about a lot of the global structure of universes, so all you really know is that the category of types in Type 0 is equivalent to the category of sets smaller than some inaccessible cardinal.

[Mario Carneiro]

yes that's definitely the case. the original model in #leantt uses a hierarchy which can be described as "a strictly monotonic sequence of inaccessible cardinals", no constraints on using the first omega inaccessibles (but you can use the first omega inaccessibles). That means there are models of lean where Type 0 has no inaccessibles in it, and other models where every universe is a Mahlo cardinal and actually supports I-R (assuming those cardinals exist).