-- Martin Escardo 2011.

module Cantor where

open import Logic
open import Naturals
open import Two
open import Equality

-- Definition (The Cantor space).

₂ℕ : Set
₂ℕ = ℕ → ₂

-- Read this as `two to the power ℕ'.