Ayberk Tosun
10 October 2022

Based directly on MartΓ­n EscardΓ³'s development from the `CantorSearch` module.

--------------------------------------------------------------------------------

In the `CantorSearch` module, the type `β„• β†’ 𝟚` is proved to be searchable for
uniformly continuous predicates. In this module, we generalise this to types
`β„• β†’ X`, where `X` is an arbitrary compact type.

\begin{code}

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

open import MLTT.Spartan
open import TypeTopology.CompactTypes
open import UF.FunExt

module TypeTopology.UniformSearch (X : 𝓀 Μ‡ )(fe : funext 𝓀₀ 𝓀) (ΞΊ : is-compactβˆ™ X) where

\end{code}

\section{Basic operations on streams}

\begin{code}

head : (β„• β†’ X) β†’ X
head u = u 0

tail : (β„• β†’ X) β†’ (β„• β†’ X)
tail u = u ∘ succ

infixr 9 _∷_

_∷_ : X β†’ (β„• β†’ X) β†’ (β„• β†’ X)
(x ∷ α) zero     = x
(x ∷ α) (succ i) = α i


cons-head-tail : (Ξ± : β„• β†’ X) β†’ head Ξ± ∷ tail Ξ± ＝ Ξ±
cons-head-tail Ξ± = dfunext fe h
 where
  h : head α ∷ tail α ∼ α
  h zero     = refl
  h (succ i) = refl

\end{code}

\section{Local constancy}

\begin{code}

_＝⟦_⟧_ : (β„• β†’ X) β†’ β„• β†’ (β„• β†’ X) β†’ 𝓀 Μ‡
π“Š ＝⟦ zero   ⟧ 𝓋 = πŸ™
π“Š ＝⟦ succ n ⟧ 𝓋 = (head π“Š ＝ head 𝓋) Γ— (tail π“Š ＝⟦ n ⟧ tail 𝓋 )

\end{code}

A map `p : ((β„• β†’ X) β†’ 𝟚)` is called *locally constant* if it has a modulus of
localy constancy.

\begin{code}

_is-a-mod-of-lc-of_ : β„• β†’ ((β„• β†’ X) β†’ 𝟚) β†’ 𝓀 Μ‡
n is-a-mod-of-lc-of p = (π“Š 𝓋 : β„• β†’ X) β†’ π“Š ＝⟦ n ⟧ 𝓋 β†’ p π“Š ＝ p 𝓋

is-locally-constant : ((β„• β†’ X) β†’ 𝟚) β†’ 𝓀 Μ‡
is-locally-constant p = Ξ£ n κž‰ β„• , n is-a-mod-of-lc-of p

\end{code}

\begin{code}

cons-decreases-mod-of-lc : (p : (β„• β†’ X) β†’ 𝟚)
                         β†’ (n : β„•)
                         β†’ (succ n) is-a-mod-of-lc-of p
                         β†’ (x : X) β†’ n is-a-mod-of-lc-of (p ∘ x ∷_)
cons-decreases-mod-of-lc p n Ο† x π“Š 𝓋 eq = Ο† (x ∷ π“Š) (x ∷ 𝓋) (refl , eq)

\end{code}

\section{Searchability}

Since `X` is assumed to be `compactβˆ™` it must be pointed. Call this point `xβ‚€`:

\begin{code}

xβ‚€ : X
xβ‚€ = compactβˆ™-types-are-pointed ΞΊ

\end{code}

There must be a selection functional `Ο΅β‚“` for `X`:

\begin{code}

X-is-compactβˆ™' : is-compactβˆ™' X
X-is-compactβˆ™' = compactβˆ™-types-are-compactβˆ™' ΞΊ

Ο΅β‚“ : (X β†’ 𝟚) β†’ X
Ο΅β‚“ = pr₁ X-is-compactβˆ™'

specification-of-Ο΅β‚“ : (p : X β†’ 𝟚)
                    β†’ p (Ο΅β‚“ p) ＝ ₁
                    β†’ (x : X) β†’ p x ＝ ₁
specification-of-Ο΅β‚“ = prβ‚‚ X-is-compactβˆ™'

\end{code}

We now define the universal quantifier for type `X` using its selection
functional

\begin{code}

βˆ€β‚“ : (X β†’ 𝟚) β†’ 𝟚
βˆ€β‚“ p = p (Ο΅β‚“ p)

specification-of-βˆ€β‚“-β‡’ : (p : X β†’ 𝟚)
                      β†’ βˆ€β‚“ p ＝ ₁
                      β†’ (x : X) β†’ p x ＝ ₁
specification-of-βˆ€β‚“-β‡’ = specification-of-Ο΅β‚“

specification-of-βˆ€β‚“-⇐ : (p : X β†’ 𝟚)
                      β†’ ((x : X) β†’ p x ＝ ₁)
                      β†’ βˆ€β‚“ p ＝ ₁
specification-of-βˆ€β‚“-⇐ p Ο† = Ο† (Ο΅β‚“ p)

\end{code}

We define the selection and universal quantification functionals for `β„• β†’ X`,
but only for locally constant predicates.

\begin{code}

Ο΅β‚™ : β„• β†’ ((β„• β†’ X) β†’ 𝟚) β†’ (β„• β†’ X)
βˆ€β‚™ : β„• β†’ ((β„• β†’ X) β†’ 𝟚) β†’ 𝟚

Ο΅β‚™ zero     p = Ξ» _ β†’ xβ‚€
Ο΅β‚™ (succ n) p = yβ‚€ ∷ Ο΅β‚™ n (Ξ» Ξ± β†’ p (yβ‚€ ∷ Ξ±))
 where
  yβ‚€ = Ο΅β‚“ Ξ» x β†’ βˆ€β‚™ n Ξ» Ξ± β†’ p (x ∷ Ξ±)

βˆ€β‚™ n p = p (Ο΅β‚™ n p)

\end{code}

Specification of `βˆ€β‚™`

\begin{code}

specification-of-βˆ€β‚™-β‡’ : (p : (β„• β†’ X) β†’ 𝟚)
                      β†’ (n : β„•)
                      β†’ n is-a-mod-of-lc-of p
                      β†’ ((π“Š : β„• β†’ X) β†’ p π“Š ＝ ₁)
                      β†’ βˆ€β‚™ n p ＝ ₁
specification-of-βˆ€β‚™-β‡’ p n ΞΆ Ο† = Ο† (Ο΅β‚™ n p)

\end{code}

\begin{code}

specification-of-βˆ€β‚™-⇐ : (p : (β„• β†’ X) β†’ 𝟚)
                      β†’ (n : β„•)
                      β†’ n is-a-mod-of-lc-of p
                      β†’ βˆ€β‚™ n p ＝ ₁
                      β†’ (π“Š : β„• β†’ X) β†’ p π“Š ＝ ₁
specification-of-βˆ€β‚™-⇐ p zero     ΞΆ Ο† π“Š = p π“Š                 ＝⟨ ΞΆ π“Š (Ξ» _ β†’ xβ‚€) ⋆ ⟩
                                         p (Ξ» _ β†’ xβ‚€)        ＝⟨ Ο†                ⟩
                                         ₁                   ∎
specification-of-βˆ€β‚™-⇐ p (succ n) ΞΆ Ο† π“Š = p π“Š                 ＝⟨ † ⟩
                                         p (head π“Š ∷ tail π“Š) ＝⟨ ‑ ⟩
                                         ₁                   ∎
 where
  x₁ : X
  x₁ = Ο΅β‚“ Ξ» y β†’ βˆ€β‚™ n (p ∘ y ∷_)

  β™  : βˆ€β‚™ n (p ∘ x₁ ∷_) ＝ ₁ β†’ (x : X) β†’ βˆ€β‚™ n (p ∘ x ∷_) ＝ ₁
  β™  = specification-of-βˆ€β‚“-β‡’ Ξ» y β†’ βˆ€β‚™ n (p ∘ y ∷_)

  IH : (x : X) β†’ βˆ€β‚™ n (p ∘ x ∷_) ＝ ₁ β†’ (𝓋 : β„• β†’ X) β†’ p (x ∷ 𝓋) ＝ ₁
  IH x = specification-of-βˆ€β‚™-⇐ (p ∘ x ∷_) n (cons-decreases-mod-of-lc p n ΞΆ x)

  † : p π“Š ＝ p (head π“Š ∷ tail π“Š)
  † = ap p (cons-head-tail π“Š ⁻¹)

  ‑ : p (head π“Š ∷ tail π“Š) ＝ ₁
  ‑ = IH (head π“Š) (β™  Ο† (head π“Š)) (tail π“Š)

\end{code}