# Cantor's diagonal argument

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

Created on 2022-02-09.

module foundation.cantors-diagonal-argument where

Imports
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


## Idea

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

## Theorem

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)

abstract
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))

abstract
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))