Chuangjie Xu 2013 (updated in February 2015)

\begin{code}

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

module UsingIrrelevantFunext.Space.Coverage where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity

\end{code}

The site we are working with is the monoid of uniformly continuous
endo-functions of the Cantor space with a coverage in which, for each
natural number n, there is a family of concatenation maps "cons s"
indexed by finite binary sequence s of length n.

The monoid of uniformly continuous ₂ℕ → ₂ℕ:

\begin{code}

C : Subset(₂ℕ  ₂ℕ)
C = uniformly-continuous-₂ℕ

\end{code}

The coverage axiom amounts to uniform continuity of endo-functions of
the Cantor space in the following sense.

\begin{code}

Theorem[Coverage-axiom] : ∀(m : )  ∀(t : ₂ℕ  ₂ℕ)  t  C 
                   Σ \(n : )  ∀(s : ₂Fin n) 
                    Σ \(s' : ₂Fin m)  Σ \(t' : ₂ℕ  ₂ℕ) 
                     (t'  C) × (∀ α  t (cons s α)  cons s' (t' α))
Theorem[Coverage-axiom] m t tC = n , prf
 where
  n : 
  n = pr₁ (tC m)
  prf : ∀(s : ₂Fin n)  Σ \(s' : ₂Fin m)  Σ \(t' : ₂ℕ  ₂ℕ) 
         (t'  C) × (∀ α  t (cons s α)  cons s' (t' α))
  prf s = s' ,  t' , t'C , e
   where
    s' : ₂Fin m
    s' = take m (t (cons s ))
    t' : ₂ℕ  ₂ℕ
    t' α = drop m (t (cons s α))
    t'C : t'  C
    t'C k = Lemma[LM-₂ℕ-least-modulus] t' l prt'
     where
      ucts : uniformly-continuous-₂ℕ (t  (cons s))
      ucts = Lemma[∘-UC] t tC (cons s) (Lemma[cons-UC] s)
      l : 
      l = pr₁ (ucts (k + m))
      prts : ∀(α β : ₂ℕ)  α ≡[ l ] β  t (cons s α) ≡[ k + m ] t (cons s β)
      prts = pr₁ (pr₂ (ucts (k + m)))
      eq : ∀(α : ₂ℕ)  ∀(i : )  t' α i  t (cons s α) (i + m)
      eq α i = Lemma[drop+] m (t (cons s α)) i
      claim₀ : ∀(α β : ₂ℕ)  α ≡[ l ] β  t (cons s α) ≡[ k + m ] t (cons s β) 
                ∀(i : )  i < k  t' α i  t' β i
      claim₀ α β el ekm i i<k = transport  b  t' α i  b) ((eq β i)⁻¹) sclaim₂
       where
        sclaim₀ : ∀(i : )  i < (k + m)  t (cons s α) i  t (cons s β) i
        sclaim₀ = Lemma[≡[]-<] ekm
        sclaim₁ : t (cons s α) (i + m)  t (cons s β) (i + m)
        sclaim₁ = sclaim₀ (i + m) (Lemma[a<b→a+c<b+c] i k m i<k)
        sclaim₂ : t' α i  t (cons s β) (i + m)
        sclaim₂ = transport  b  b  t (cons s β) (i + m)) ((eq α i)⁻¹) sclaim₁
      claim₁ : ∀(α β : ₂ℕ)  α ≡[ l ] β
              t (cons s α) ≡[ k + m ] t (cons s β)  t' α ≡[ k ] t' β
      claim₁ α β el ekm = Lemma[<-≡[]] (claim₀ α β el ekm)
      prt' : ∀(α β : ₂ℕ)  α ≡[ l ] β  t' α ≡[ k ] t' β
      prt' α β el = claim₁ α β el (prts α β el)
    e : ∀(α : ₂ℕ)  ∀(i : )  t (cons s α) i  cons s' (t' α) i
    e α i = transport  x  t (cons s α) i  cons x (t' α) i) claim₂ claim₀
     where
      claim₀ : t (cons s α) i  cons (take m (t (cons s α))) (t' α) i
      claim₀ = (Lemma[cons-take-drop] m (t (cons s α)) i)⁻¹
      claim₁ : t (cons s α) ≡[ m ] t (cons s )
      claim₁ = pr₁ (pr₂ (tC m)) (cons s α) (cons s ) (Lemma[cons-≡[]] s α )
      claim₂ : take m (t (cons s α))  s'
      claim₂ = Lemma[≡[]-take] claim₁

\end{code}