The type of bit streams is uncountable.

Corey.agda

open import Data.Bool
open import Data.Empty
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality

module Corey where

  -- streams of bits
  record Stream : Set where
    coinductive
    field
      hd : Bool
      tl : Stream

  open Stream

  -- the n-th term of a Stream
  infix 5 _‼_

  _‼_ : Stream → Nat → Bool
  s ‼ zero = hd s
  s ‼ (suc n) = tl s ‼ n

  -- the tail of a sequence
  shift : ∀ {A : Set} → (Nat → A) → (Nat → A)
  shift e n = e (suc n)

  -- convert a sequence to a stream
  str : (Nat → Bool) → Stream
  hd (str f) = f zero
  tl (str f) = str (shift f)

  -- str respects positions
  str-‼ : ∀ (e : Nat → Bool) (n : Nat) → str e ‼ n ≡ e n
  str-‼ e zero = refl
  str-‼ e (suc n) = str-‼ (shift e) n

  -- Cantor's diagonalization of a sequence of streams
  diagonalize : (Nat → Stream) → Stream
  diagonalize e = str (λ n → not (e n ‼ n))

  -- This probably exists in a library somewhere
  not-≢ : ∀ b → b ≢ not b
  not-≢ false ()
  not-≢ true ()

  -- Streams cannot be exhausted by a sequence
  cantor : ∀ (e : Nat → Stream) → ∀ n → e n ≢ diagonalize e
  cantor e n ξ =
    not-≢
      (e n ‼ n)
      (trans (cong (_‼ n) ξ) (str-‼ (λ n → not (e n ‼ n)) n))