Cantor's diagonal argument

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-09.
Last modified on 2024-02-06.

module foundation.cantors-diagonal-argument where
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.surjective-maps
open import foundation.universe-levels

open import foundation-core.empty-types
open import foundation-core.fibers-of-maps
open import foundation-core.propositions


Cantor's diagonal argument is used to show that there is no surjective map from a type into the type of its subtypes.


map-cantor :
  {l1 l2 : Level} (X : UU l1) (f : X  (X  Prop l2))  (X  Prop l2)
map-cantor X f x = neg-Prop (f x x)

  not-in-image-map-cantor :
    {l1 l2 : Level} (X : UU l1) (f : X  (X  Prop l2)) 
    ( t : fiber f (map-cantor X f))  empty
  not-in-image-map-cantor X f (pair x α) =
    no-fixed-points-neg-Prop (f x x) (iff-eq (htpy-eq α x))

  cantor :
    {l1 l2 : Level} (X : UU l1) (f : X  X  Prop l2)  ¬ (is-surjective f)
  cantor X f H =
    ( apply-universal-property-trunc-Prop
      ( H (map-cantor X f))
      ( empty-Prop)
      ( not-in-image-map-cantor X f))

Recent changes