Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

module Cantor where

open import Naturals
open import Two

\end{code}

Definition (The Cantor space):

\begin{code}

₂ℕ : Set
₂ℕ =   

open import DiscreteAndSeparated

₂ℕ-separated : separated ₂ℕ
₂ℕ-separated = separated-ideal _  ₂-separated)

\end{code}