Skip to content

Unsafe.CantorCompact

Martin Escardo 2011.

The Cantor space is the type (β„• β†’ 𝟚). We show it is compact, under
the assumptions discussed in CountableTychonoff.

This module is a set of corollaries of the module CountableTychonoff
and other modules.


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

open import UF.FunExt

module Unsafe.CantorCompact (fe : FunExt) where

open import MLTT.Spartan
open import MLTT.Two-Properties

open import TypeTopology.CompactTypes

open import Unsafe.CountableTychonoff fe

cantor-compactβˆ™ : is-compactβˆ™ (β„• β†’ 𝟚)
cantor-compactβˆ™ = countable-Tychonoff (Ξ» i β†’ 𝟚-is-compactβˆ™)

cantor-compact : is-compact (β„• β†’ 𝟚)
cantor-compact = compactβˆ™-types-are-compact cantor-compactβˆ™

cantor-wcompact : is-wcompact (β„• β†’ 𝟚)
cantor-wcompact = compact-gives-wcompact cantor-compactβˆ™


The characteristic function of the universal quantifier
of the Cantor space:


A : ((β„• β†’ 𝟚) β†’ 𝟚) β†’ 𝟚
A = pr₁ (wcompact-types-are-wcompact' cantor-wcompact)


Discreteness of ((β„• β†’ 𝟚) β†’ β„•):


open import UF.DiscreteAndSeparated

Cantorβ†’β„•-is-discrete : is-discrete ((β„• β†’ 𝟚) β†’ β„•)
Cantorβ†’β„•-is-discrete = discrete-to-power-compact-is-discrete' (fe 𝓀₀ 𝓀₀)
                        cantor-compact
                        β„•-is-discrete


The characteristic function of equality on ((β„• β†’ 𝟚) β†’ β„•):


open import NotionsOfDecidability.Complemented

equal : ((β„• β†’ 𝟚) β†’ β„•) β†’ ((β„• β†’ 𝟚) β†’ β„•) β†’ 𝟚

equal f  = pr₁ (characteristic-function (Cantorβ†’β„•-is-discrete f))


Experiments: Evaluate the following to normal form (give β‚€, ₁, ₁, β‚€ quickly):


number : 𝟚 β†’ β„•
number β‚€ = 0
number ₁ = 1

test0 : 𝟚
test0 = A (Ξ» Ξ± β†’ min𝟚 (Ξ± 17) (Ξ± 180))

test1 : 𝟚
test1 = A (Ξ» Ξ± β†’ ₁)

test2 : 𝟚
test2 = equal (Ξ» Ξ± β†’ number (Ξ± 17)) (Ξ» Ξ± β†’ number (Ξ± 100))

test3 : 𝟚
test3 = equal (Ξ» Ξ± β†’ number (Ξ± 100)) (Ξ» Ξ± β†’ number (Ξ± 100))

test4 : 𝟚
test4 = equal (Ξ» Ξ± β†’ number (Ξ± 1000)) (Ξ» Ξ± β†’ number (Ξ± 1000))

test5 : 𝟚
test5 = equal (Ξ» Ξ± β†’ number (Ξ± 1001)) (Ξ» Ξ± β†’ number (Ξ± 1000))