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 β