A generalization of Cantor's diagonalization argument.

cantor.agda

module cantor where
open import Data.Product
open import Data.Empty
open import Level

-- A variant of (https://coq.inria.fr/refman/language/core/inductive.html?highlight=cantor)

-- Sort of spooky this works.
data _≡_ {ℓ : Level}{A : Set ℓ} : A → A → Set₀ where
  refl : (a : A) → a ≡ a

fcong : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'}(f g : A → B) → f ≡ g → (a : A) → f a ≡ g a
fcong  f g (refl ._) _ = refl _

coe : {ℓ ℓ' : Level}{A : Set ℓ}(P : A → Set ℓ') → (a b : A) → a ≡ b → P a → P b
coe P a b (refl ._) x = x

{-# NO_UNIVERSE_CHECK #-}
record Forall (A : Set₁) (P : A → Set) : Set where
  constructor lambda
  field
    app : (a : A) → (P a)
open Forall

All = Forall Set
postulate All/inj : ∀ {P Q} → All P ≡ All Q → P ≡ Q

Exists : (A : Set₁)(P : A → Set) → Set
Exists A P = All λ C → (Forall A λ a → P a → C) → C

mk : {A : Set₁}(P : A → Set)(a : A) → P a → Exists A P
mk P A p = lambda (λ C f → app f A p)

Diag : (X : Set) → Set
Diag X =
  Exists (Set → Set) λ s →
  (All s ≡ X) × (s X → ⊥)

Fixed : Set
Fixed = All Diag

cantor₁ : Diag Fixed → (Diag Fixed → ⊥)
cantor₁ df₀ =
  app
  df₀
  (Diag Fixed → ⊥)
  (lambda λ s (Fixed≡Alls , sFixed→⊥) →
    let
      eq : s ≡ Diag
      eq = All/inj Fixed≡Alls

      eq2 : s Fixed ≡ Diag Fixed
      eq2 = fcong _ _ eq Fixed
    in
    coe (λ A → A → ⊥) _ _ eq2 sFixed→⊥)

cantor₂ : (Diag Fixed → ⊥) → Diag Fixed
cantor₂ contra = mk _ Diag (refl _ , contra)

bad : ⊥
bad = cantor₁ (cantor₂ λ x → cantor₁ x x) (cantor₂ λ x → cantor₁ x x)