English
There is no surjection from any α to Type(max u v). This shows why Type : Type would be inconsistent.
Русский
Не существует сюръективности из любого типа α в Type(max u v). Это демонстрирует, почему Type : Type было бы противоречиво.
LaTeX
$$$\forall \alpha: \text{Type}_u,\ f: \alpha \to \text{Type}(\max u v),\ \lnot \operatorname{Surjective}(f).$$$
Lean4
/-- There is no surjection from `α : Type u` into `Type (max u v)`. This theorem
demonstrates why `Type : Type` would be inconsistent in Lean. -/
theorem not_surjective_Type {α : Type u} (f : α → Type max u v) : ¬Surjective f :=
by
intro hf
let T : Type max u v := Sigma f
cases hf (Set T) with
| intro U hU =>
let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
have hg : Injective g := by
intro s t h
suffices cast hU (g s).2 = cast hU (g t).2
by
simp only [g, cast_cast, cast_eq] at this
assumption
· congr
exact cantor_injective g hg
