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.