Martin Escardo 2011.

\begin{code}

module Cantor where

open import Naturals
open import Two

\end{code}

Definition (The Cantor space):

\begin{code}

₂ℕ : Set
₂ℕ = ℕ → ₂

\end{code}