Cantor

Martin Escardo and Paulo Oliva 2011


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

module InfinitePigeon.Cantor where

open import InfinitePigeon.Naturals
open import InfinitePigeon.Two

₂ℕ : Set
₂ℕ = ℕ → ₂