Skip to content

Instantly share code, notes, and snippets.

@AndrasKovacs

AndrasKovacs/Cantor.agda

Created August 6, 2020 13:57
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save AndrasKovacs/0f35b6598e560faf3a0bfc1f0ceaac6e to your computer and use it in GitHub Desktop.
Save AndrasKovacs/0f35b6598e560faf3a0bfc1f0ceaac6e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Cantor.agda
{-# OPTIONS --without-K #-}
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Function
surj : {A B : Set} → (A → B) → Set
surj f = ∀ b → ∃ λ a → f a ≡ b
pow : Set → Set
pow A = A → Bool
cantor : ∀ {A}(f : A → pow A) → surj f → ⊥
cantor f p with p (λ n → not (f n n))
... | a , q with cong (λ f → f a) q
... | r with f a a
... | true = case r of λ ()
... | false = case r of λ ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment