module Cantor where

open import Naturals
open import Two

₂ℕ : Set
₂ℕ = ℕ → ₂