Skip to content

Instantly share code, notes, and snippets.

@moleike
Forked from jozefg/cantor.agda
Created April 25, 2025 15:30
Show Gist options
  • Save moleike/16b6da53f99c4d8bb9c89a9db7bf2b54 to your computer and use it in GitHub Desktop.
Save moleike/16b6da53f99c4d8bb9c89a9db7bf2b54 to your computer and use it in GitHub Desktop.
A generalization of Cantor's diagonalization argument.
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment