module Cantor where

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

-- Definition (The Cantor space).
₂ℕ : Set
₂ℕ =   

-- Definition (Extensional equality on the Cantor space).
_≣_ : (α β : ₂ℕ)   Ω
α  β =  i  α i  β i 


-- Basic facts.

≣-refl : 
-------------------
  ∀{α : ₂ℕ}  α  α
-------------------  
≣-refl i = refl


≣-symmetry : 
-----------------------------
  ∀{α β : ₂ℕ}  α  β  β  α
-----------------------------
≣-symmetry e i = symmetry (e i)


≣-transitivity : 
---------------------------------------
  ∀{α β γ : ₂ℕ}  α  β  β  γ  α  γ
---------------------------------------
≣-transitivity r s i = transitivity (r i) (s i)


-- Definition (Extensional ₂-valued functions on the Cantor space).
extensional : (₂ℕ  )  Ω
extensional p = ∀{α β : ₂ℕ}  α  β  p α  p β