contradiction from retract existence

Stream: Is there code for X?

[Asei Inoue]

axiom U : Type

-- I want to assume `Type : Type` but
-- Lean doesn't allow me to do so.
-- Then I will assume slightly weaker hypothesises...

axiom down (T : Type) : U
axiom up (u : U) : Type

-- There is a retract from Type to U
axiom retract (T : Type) : up (down T) = T

-- I want to show this
theorem paradox : False := by
  sorry

[Asei Inoue]

My attempt: Trivially up is a surjective map.
by Cantor theorem, there is no surjective map from U to Set U. so it is sufficient to show that there is a surjective map from Type to Set U.

[Markus Himmel]

Here is one way:

import Mathlib

axiom U : Type

-- I want to assume `Type : Type` but
-- Lean doesn't allow me to do so.
-- Then I will assume slightly weaker hypothesises...

axiom down (T : Type) : U
axiom up (u : U) : Type

-- There is a retract from Type to U
axiom retract (T : Type) : up (down T) = T

-- I want to show this
theorem paradox : False :=
  not_small_type.{0} ⟨Set.range down, ⟨Equiv.ofInjective down (Function.LeftInverse.injective retract)⟩⟩

[Asei Inoue]

what is not_small_type?

[Markus Himmel]

docs#not_small_type says that there is no equivalence α ≃ Type for any α : Type.

[Markus Himmel]

Even more direct:

theorem paradox : False :=
  Function.not_surjective_Type up (Function.RightInverse.surjective retract)