§ There cannot be a type of size the universe

axiom CODE : Type -- assume we have CODEs for types...
axiom decode : CODE -> Type -- and a decoding...
axiom decode_surjective: ∀ (t: Type), { code: CODE // decode code = t } -- which is surjective on types.
abbrev Powerset (X: Type) := X -> Prop -- the powerset of a type is the collection of all subsets.

abbrev codedU := Σ (code: CODE), decode code -- create the set of all values that are reachable by decoding the codes...
abbrev UcodedU := Powerset codedU -- build its powerset...
noncomputable def codedUcodedU: { code_UcodedU : CODE //  decode code_UcodedU = UcodedU } := by { -- encode this...
  apply decode_surjective;
}
noncomputable def cantor (UcodedU: Powerset codedU): codedU := -- use the fact that the UcodedU has a code....
    ⟨ codedUcodedU.val, by { have H := codedUcodedU.property; simp[H]; exact UcodedU } ⟩
-- Now run cantor diagonalization.