Show there is no bijection from A to 2^A

omega.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl y = y

data Bool : Set where
  False True : Bool

not : Bool → Bool
not False = True
not True = False

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

data Dec (A : Set) : Set where
  yes : A → Dec A
  no  : (A → ⊥) → Dec A

natEq : (n m : ℕ) → Dec (n ≡ m)
natEq zero zero = yes refl
natEq zero (suc m) = no (λ ())
natEq (suc n) zero = no (λ ())
natEq (suc n) (suc m) with natEq n m
...                   | yes refl = yes refl
...                   | no  neq  = no φ
                                   where φ : _
                                         φ refl = neq refl

consistent : {x : Bool} → x ≡ not x → ⊥
consistent {False} ()
consistent {True} ()

2^_ : (A : Set) → Set
2^_ A = A → Bool

record Diagonal {T : ℕ → Set} {n : ℕ} (f : T n → (2^ (Σ ℕ T))) : Set where
  constructor diagonal
  field
    value : 2^ (Σ ℕ T)
    distinct : (x : T n) → f x ≡ value → ⊥

agreeAt : {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
agreeAt refl k = refl

diagonalisevalue : {T : ℕ → Set} {n : ℕ} (f : T n → (2^ (Σ ℕ T))) → 2^ (Σ ℕ T)
diagonalisevalue {T} {n} f (m , x) with natEq n m
diagonalisevalue {T} {.m} f (m , x) | yes refl = not (f x (m , x))
diagonalisevalue {T} {n} f (m , x) | no x₁ = False

diagonalisedistinct : {T : ℕ → Set} {n : ℕ} (f : T n → (2^ (Σ ℕ T))) → (x : T n) → f x ≡ (diagonalisevalue f) → ⊥
diagonalisedistinct {T} {n} f x eq = consistent bad
  where
    bad' : f x (n , x) ≡ diagonalisevalue f (n , x)
    bad' = agreeAt {Σ ℕ T} {Bool} {f x} {diagonalisevalue f} eq (n , x)
    help : diagonalisevalue f (n , x) ≡ not (f x (n , x))
    help with natEq n n
    help | yes refl = refl
    help | no x = ⊥-elim (x refl)
    bad : f x (n , x) ≡ not (f x (n , x))
    bad = trans bad' help

diagonalise : {T : ℕ → Set} {n : ℕ} (f : T n → (2^ (Σ ℕ T))) → Diagonal f
Diagonal.value (diagonalise f) = diagonalisevalue f
Diagonal.distinct (diagonalise f) = diagonalisedistinct f

record Bijection (A B : Set) : Set where
  constructor bijection
  field
    fun : A → B
    inj : (x y : A) → fun x ≡ fun y → x ≡ y
    sur : (y : B) → Σ A λ x → fun x ≡ y

identbiject : {A B : Set} → A ≡ B → Bijection A B
Bijection.fun (identbiject {A} {.A} refl) x = x
Bijection.inj (identbiject {A} {.A} refl) x .x refl = refl
fst (Bijection.sur (identbiject {A} {.A} refl) y) = y
snd (Bijection.sur (identbiject {A} {.A} refl) y) = refl

no-bijection : {T : ℕ → Set} {n : ℕ} → Bijection (T n) (2^ (Σ ℕ T)) → ⊥
no-bijection (bijection fun inj sur) with diagonalise fun
... | diagonal value distinct = distinct (Σ.fst (sur value)) (Σ.snd (sur value))

newtype : (T : ℕ → Set) → Σ Set (λ A → ∀ n → T n ≡ A → ⊥)
fst (newtype T) = 2^ (Σ ℕ T)
snd (newtype T) n eq = no-bijection (identbiject eq)

one.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

data Bool : Set where
  False True : Bool

not : Bool → Bool
not False = True
not True = False

data ⊥ : Set where

consistent : {x : Bool} → x ≡ not x → ⊥
consistent {False} ()
consistent {True} ()

2^_ : (A : Set) → Set
2^_ A = A → Bool

record Diagonal {A : Set} (f : A → (2^ A)) : Set where
  constructor diagonal
  field
    value : 2^ A
    distinct : (x : A) → f x ≡ value → ⊥

extensional : {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
extensional refl k = refl

diagonalise : {A : Set} → (f : A → (2^ A)) → Diagonal f
Diagonal.value (diagonalise f) x = not (f x x)
Diagonal.distinct (diagonalise f) x eq = consistent (extensional eq x)

record Bijection (A B : Set) : Set where
  constructor bijection
  field
    fun : A → B
    inj : (x y : A) → fun x ≡ fun y → x ≡ y
    sur : (y : B) → Σ A λ x → fun x ≡ y

identbiject : {A B : Set} → A ≡ B → Bijection A B
Bijection.fun (identbiject {A} {.A} refl) x = x
Bijection.inj (identbiject {A} {.A} refl) x .x refl = refl
fst (Bijection.sur (identbiject {A} {.A} refl) y) = y
snd (Bijection.sur (identbiject {A} {.A} refl) y) = refl

no-bijection : (A : Set) → Bijection A (2^ A) → ⊥
no-bijection A (bijection fun inj sur) with diagonalise fun
... | diagonal value distinct = distinct (Σ.fst (sur value)) (Σ.snd (sur value))

newtype : (A : Set) → Σ Set (λ B → A ≡ B → ⊥)
fst (newtype A) = 2^ A
snd (newtype A) x = no-bijection A (identbiject x)

two.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

record Σ {A : Set} (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

data Bool : Set where
  False True : Bool

not : Bool → Bool
not False = True
not True = False

data ⊥ : Set where

consistent : {x : Bool} → x ≡ not x → ⊥
consistent {False} ()
consistent {True} ()

2^_ : (A : Set) → Set
2^_ A = A → Bool

record Diagonal {A B : Set} (f : A → (2^ B)) : Set where
  constructor diagonal
  field
    value : 2^ B
    distinct : (x : A) → f x ≡ value → ⊥

extensional : {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
extensional refl k = refl

diagonalise : {A B : Set} → (f : A → (2^ (A ⊎ B))) → Diagonal f
Diagonal.value (diagonalise f) (inl x) = not (f x (inl x))
Diagonal.value (diagonalise f) (inr x) = False
Diagonal.distinct (diagonalise f) x eq = consistent (extensional eq (inl x))

record Bijection (A B : Set) : Set where
  constructor bijection
  field
    fun : A → B
    inj : (x y : A) → fun x ≡ fun y → x ≡ y
    sur : (y : B) → Σ λ x → fun x ≡ y

no-bijection : (A B : Set) → Bijection A (2^ (A ⊎ B)) → ⊥
no-bijection A B (bijection fun inj sur) with diagonalise fun
... | diagonal value distinct = distinct (Σ.fst (sur value)) (Σ.snd (sur value))