Chuangjie Xu 2013 (updated in February 2015)

The axiom of uniform continuity is not provable in HAω. But it can be
realized in our model by the following Fan functional:

       fan : Map ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ℕSpace

which continuously computes the least moduli of uniform continuity.

\begin{code}

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

module UsingIrrelevantFunext.Space.Fan where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingIrrelevantFunext.Irrelevance
open import UsingIrrelevantFunext.Space.Coverage
open import UsingIrrelevantFunext.Space.Space
open import UsingIrrelevantFunext.Space.CartesianClosedness
open import UsingIrrelevantFunext.Space.DiscreteSpace
open import UsingIrrelevantFunext.Space.YonedaLemma
open import UsingIrrelevantFunext.IrrelevantFunext

\end{code}

To show the continuity of the fan functional, we need the following auxiliaries.

\begin{code}

_×2 : ℕ → ℕ
_×2 0        = 0
_×2 (succ n) = succ (succ (n ×2))

Lemma[n≤2n] : ∀(n : ℕ) → n ≤ (n ×2)
Lemma[n≤2n] 0        = ≤-zero
Lemma[n≤2n] (succ n) = ≤-trans (≤-succ (Lemma[n≤2n] n)) (Lemma[n≤n+1] (succ (n ×2)))

Lemma[n<m→2n<2m] : ∀(n m : ℕ) → n < m → (n ×2) < (m ×2)
Lemma[n<m→2n<2m] 0        0        ()
Lemma[n<m→2n<2m] 0        (succ m) _          = ≤-succ ≤-zero
Lemma[n<m→2n<2m] (succ n) 0        ()
Lemma[n<m→2n<2m] (succ n) (succ m) (≤-succ r) = ≤-succ (≤-succ (Lemma[n<m→2n<2m] n m r))


_×2+1 : ℕ → ℕ
_×2+1 0        = 1
_×2+1 (succ n) = succ (succ (n ×2+1))

Lemma[n≤2n+1] : ∀(n : ℕ) → n ≤ (n ×2+1)
Lemma[n≤2n+1] 0        = ≤-zero
Lemma[n≤2n+1] (succ n) = ≤-trans (≤-succ (Lemma[n≤2n+1] n)) (Lemma[n≤n+1] (succ (n ×2+1)))

Lemma[n<m→2n+1<2m+1] : ∀(n m : ℕ) → n < m → (n ×2+1) < (m ×2+1)
Lemma[n<m→2n+1<2m+1] 0        0        ()
Lemma[n<m→2n+1<2m+1] 0        (succ m) _          = ≤-succ (≤-succ ≤-zero)
Lemma[n<m→2n+1<2m+1] (succ n) 0        ()
Lemma[n<m→2n+1<2m+1] (succ n) (succ m) (≤-succ r) = ≤-succ (≤-succ (Lemma[n<m→2n+1<2m+1] n m r))


\end{code}

Here is the fan functional, which calculates smallest moduli, using
the moduli obtained by Yoneda Lemma.

\begin{code}


fan : Map ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ℕSpace
fan = f , cts
 where
  f : U((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) → ℕ
  f φ = pr₁ (pr₂ (Lemma[Yoneda] ℕSpace φ))
  cts : continuous ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ℕSpace f
  cts p pr = Lemma[LM-ℕ-least-modulus] (f ∘ p) n prf
   where
    t₀ : ₂ℕ → ₂ℕ
    t₀ α = α ∘ _×2
    uct₀ : t₀ ∈ C
    uct₀ m = Lemma[LM-₂ℕ-least-modulus] t₀ (m ×2) prf₁
     where
      prf₀ : ∀(α β : ₂ℕ) → α ≡[ m ×2 ] β → ∀(i : ℕ) → i < m → t₀ α i ≡ t₀ β i
      prf₀ α β aw i i<m = Lemma[≡[]-<] aw (i ×2) (Lemma[n<m→2n<2m] i m i<m)
      prf₁ : ∀(α β : ₂ℕ) → α ≡[ m ×2 ] β → t₀ α ≡[ m ] t₀ β
      prf₁ α β aw = Lemma[<-≡[]] (prf₀ α β aw)

    t₁ : ₂ℕ → ₂ℕ
    t₁ α = α ∘ _×2+1
    uct₁ : t₁ ∈ C
    uct₁ m = Lemma[LM-₂ℕ-least-modulus] t₁ (m ×2+1) prf₁ 
     where
      prf₀ : ∀(α β : ₂ℕ) → α ≡[ m ×2+1 ] β → ∀(i : ℕ) → i < m → t₁ α i ≡ t₁ β i
      prf₀ α β aw i i<m = Lemma[≡[]-<] aw (i ×2+1) (Lemma[n<m→2n+1<2m+1] i m i<m)
      prf₁ : ∀(α β : ₂ℕ) → α ≡[ m ×2+1 ] β → t₁ α ≡[ m ] t₁ β
      prf₁ α β aw = Lemma[<-≡[]] (prf₀ α β aw)

    t₁' : ₂ℕ → U(ℕSpace ⇒ ₂Space)
    t₁' = pr₁ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] t₁ uct₁)
    prf₁ : t₁' ∈ Probe (ℕSpace ⇒ ₂Space)
    prf₁ = pr₂ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] t₁ uct₁)

    merge : ₂ℕ → ₂ℕ → ₂ℕ
    merge α β 0               = α 0
    merge α β 1               = β 0
    merge α β (succ (succ i)) = merge (α ∘ succ) (β ∘ succ) i

    lemma' : ∀(α β γ : ₂ℕ) → ∀(k : ℕ) → α ≡[ k ] β → ∀(i : ℕ) → i < (k ×2)
           → merge α γ i ≡ merge β γ i
    lemma' α β γ 0        aw i ()
    lemma' α β γ (succ k) aw 0 r = Lemma[≡[]-<] aw zero (≤-succ ≤-zero)
    lemma' α β γ (succ k) aw 1 r = refl
    lemma' α β γ (succ k) aw (succ (succ i)) (≤-succ (≤-succ r)) =
          lemma' (α ∘ succ) (β ∘ succ) (γ ∘ succ) k (Lemma[≡[]-succ] aw) i r

    lemma : ∀(α β γ : ₂ℕ) → ∀(k : ℕ) → α ≡[ k ] β → merge α γ ≡[ k ×2 ] merge β γ
    lemma α β γ k ek = Lemma[<-≡[]] (lemma' α β γ k ek)

    lemma₀ : ∀(α β : ₂ℕ) → [ t₀ (merge α β) ≡ α ]
    lemma₀ α β = funext¹ (le α β)
                 -------
     where
      le : ∀(α β : ₂ℕ) → ∀(i : ℕ) → t₀ (merge α β) i ≡ α i
      le α β 0        = refl
      le α β (succ i) = le (α ∘ succ) (β ∘ succ) i

    lemma₁ : ∀(α β : ₂ℕ) → ∀(i : ℕ) → t₁ (merge α β) i ≡ β i
    lemma₁ α β 0        = refl
    lemma₁ α β (succ i) = lemma₁ (α ∘ succ) (β ∘ succ) i

    lemma₁' : ∀(α : ₂ℕ) → ∀(φ : Map ℕSpace ₂Space) →
               [ t₁' (merge α (pr₁  φ)) ≡ φ ]
    lemma₁' α (γ , ctsγ) = Lemma[Map-₂-[≡]] ℕSpace (β , ctsβ) (γ , ctsγ) claim
     where
      β : ₂ℕ
      β = pr₁ (t₁' (merge α γ))
      ctsβ : continuous ℕSpace ₂Space β
      ctsβ = pr₂ (t₁' (merge α γ))
      claim : ∀(i : ℕ) → β i ≡ γ i
      claim = lemma₁ α γ 

    q : ₂ℕ → ℕ
    q α = (pr₁ ∘ p)(t₀ α)(t₁' α)
    ucq : locally-constant q
    ucq = pr t₁' prf₁ t₀ uct₀

    n : ℕ
    n = pr₁ ucq

    claim : ∀(α β : ₂ℕ) → α ≡[ n ] β → [ p α ≡ p β ]
    claim α β en = Lemma[Map-ℕ-[≡]] (ℕSpace ⇒ ₂Space) (pα , ctsα) (pβ , ctsβ) sclaim
     where
      pα : Map ℕSpace ₂Space → ℕ
      pα = pr₁ (p α)
      ctsα : continuous (ℕSpace ⇒ ₂Space) ℕSpace pα
      ctsα = pr₂ (p α)
      pβ : Map ℕSpace ₂Space → ℕ
      pβ = pr₁ (p β)
      ctsβ : continuous (ℕSpace ⇒ ₂Space) ℕSpace pβ
      ctsβ = pr₂ (p β)
      sclaim : ∀(γ : Map ℕSpace ₂Space) → pα γ ≡ pβ γ
      sclaim (γ , ctsγ) = decidable-structure (ℕ-discrete (pα (γ , ctsγ)) (pβ (γ , ctsγ))) ssclaim₄
       where
        eγ : merge α γ ≡[ n ] merge β γ
        eγ = Lemma[≡[]-≤] (lemma α β γ n en) (Lemma[n≤2n] n)
        ssclaim₀ : [ (pr₁ ∘ p)(t₀ (merge α γ))(t₁' (merge α γ))
                   ≡ (pr₁ ∘ p)(t₀ (merge β γ))(t₁' (merge β γ)) ]
        ssclaim₀ = hide (pr₁ (pr₂ ucq) (merge α γ) (merge β γ) eγ)
        ssclaim₁ : [ (pr₁ ∘ p)(α)(t₁' (merge α γ))
                   ≡ (pr₁ ∘ p)(t₀ (merge β γ))(t₁' (merge β γ)) ]
        ssclaim₁ = [transport] (λ x → (pr₁ ∘ p)(x)(t₁' (merge α γ))
                                    ≡ (pr₁ ∘ p)(t₀ (merge β γ))(t₁' (merge β γ)))
                               (lemma₀ α γ) ssclaim₀
        ssclaim₂ : [ pr₁ (p α) (t₁' (merge α γ)) ≡ pr₁ (p β) (t₁' (merge β γ)) ]
        ssclaim₂ = [transport] (λ x → (pr₁ ∘ p)(α)(t₁' (merge α γ)) ≡ (pr₁ ∘ p)(x)(t₁' (merge β γ)))
                               (lemma₀ β γ) ssclaim₁
        ssclaim₃ : [ pr₁ (p α) (γ , ctsγ) ≡ pr₁ (p β) (t₁' (merge β γ)) ]
        ssclaim₃ = [transport] (λ x → pr₁ (p α) (x) ≡ pr₁ (p β) (t₁' (merge β γ)))
                               (lemma₁' α (γ , ctsγ)) ssclaim₂
        ssclaim₄ : [ pr₁ (p α) (γ , ctsγ) ≡ pr₁ (p β) (γ , ctsγ) ]
        ssclaim₄ = [transport] (λ x → pr₁ (p α) (γ , ctsγ) ≡ pr₁ (p β) (x))
                               (lemma₁' β (γ , ctsγ)) ssclaim₃

    prf : ∀(α β : ₂ℕ) → α ≡[ n ] β → (f ∘ p) α ≡ (f ∘ p) β
    prf α β en = Lemma[[≡]→≡]-ℕ ([ap] f (claim α β en))


fan-behaviour : ∀(f : U ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace)) →
                ∀(α β : U (ℕSpace ⇒ ₂Space)) → pr₁ α ≡[ pr₁ fan f ] pr₁ β → pr₁ f α ≡ pr₁ f β
fan-behaviour f α β r = Lemma[[≡]→≡]-ℕ [goal]
 where
  f' : ₂ℕ → ℕ
  f' = pr₁ (Lemma[Yoneda] ℕSpace f)
  claim : [ f' (pr₁ α) ≡ f' (pr₁ β) ]
  claim = hide (pr₁(pr₂ (pr₂ (Lemma[Yoneda] ℕSpace f))) (pr₁ α) (pr₁ β) r)
  eqα : [ pr₁ f α ≡ f' (pr₁ α) ]
  eqα = [ap] (pr₁ f) (Lemma[ID-[≡]] α)
  eqβ : [ pr₁ f β ≡ f' (pr₁ β) ]
  eqβ = [ap] (pr₁ f) (Lemma[ID-[≡]] β)
  [goal] : [ pr₁ f α ≡ pr₁ f β ]
  [goal] = [trans] ([trans] eqα claim) ([sym] eqβ)

\end{code}