Chuangjie Xu 2013 (updated in February 2015)

The axiom of uniform continuity is not provable in HAω, but 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 UsingSetoid.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 UsingSetoid.Setoid
open import UsingSetoid.Space.Coverage
open import UsingSetoid.Space.Space
open import UsingSetoid.Space.CartesianClosedness
open import UsingSetoid.Space.DiscreteSpace
open import UsingSetoid.Space.YonedaLemma

\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 = (∣fan∣ , ef) , cts
 where
  ∣fan∣ : G((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) → ℕ
  ∣fan∣ φ = pr₁ (pr₂ (Lemma[Yoneda] ℕSpace φ))

  ef : ∀ φ φ' → (∀ α → pr₁ (pr₁ φ) α ≡ pr₁ (pr₁ φ') α) → ∣fan∣ φ ≡ ∣fan∣ φ'
  ef φ φ' eφ = goal
   where
    p : ₂ℕ → ℕ
    p = pr₁ (pr₁ (Lemma[Yoneda] ℕSpace φ))
    prf : ∀ α β → α ≡[ ∣fan∣ φ ] β → p α ≡ p β
    prf = pr₁ (pr₂ (pr₂ (Lemma[Yoneda] ℕSpace φ)))
    min : ∀ n → (∀ α β → α ≡[ n ] β → p α ≡ p β) → ∣fan∣ φ ≤ n
    min = pr₂ (pr₂ (pr₂ (Lemma[Yoneda] ℕSpace φ)))
    p' : ₂ℕ → ℕ
    p' = pr₁ (pr₁ (Lemma[Yoneda] ℕSpace φ'))
    prf' : ∀ α β → α ≡[ ∣fan∣ φ' ] β → p' α ≡ p' β
    prf' = pr₁ (pr₂ (pr₂ (Lemma[Yoneda] ℕSpace φ')))
    min' : ∀ n → (∀ α β → α ≡[ n ] β → p' α ≡ p' β) → ∣fan∣ φ' ≤ n
    min' = pr₂ (pr₂ (pr₂ (Lemma[Yoneda] ℕSpace φ')))
    ep : ∀ α → p α ≡ p' α
    ep α = eφ ((α , Lemma[₂ℕ-E-map] α) , 
               Lemma[discrete-ℕSpace] ₂Space (α , Lemma[₂ℕ-E-map] α))
    pr : ∀ α β → α ≡[ ∣fan∣ φ ] β → p' α ≡ p' β
    pr α β e = (ep α)⁻¹ · prf α β e · ep β
    pr' : ∀ α β → α ≡[ ∣fan∣ φ' ] β → p α ≡ p β
    pr' α β e = ep α · prf' α β e · (ep β)⁻¹
    goal : ∣fan∣ φ ≡ ∣fan∣ φ'
    goal = Lemma[m≤n∧n≤m→m=n] (min (∣fan∣ φ') pr') (min' (∣fan∣ φ) pr)

  cts : continuous ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ℕSpace (∣fan∣ , ef)
  cts (p , ep) pr = Lemma[LM-ℕ-least-modulus] (∣fan∣ ∘ p) n prf
   where
    t₀ : ₂ℕ → ₂ℕ
    t₀ α = α ∘ _×2
    et₀ : ∀(α β : ₂ℕ) → α ≣ β → t₀ α ≣ t₀ β
    et₀ α β e i = e (i ×2)
    uct₀ : (t₀ , et₀) ∈ 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
    et₁ : ∀(α β : ₂ℕ) → α ≣ β → t₁ α ≣ t₁ β
    et₁ α β e i = e (i ×2+1)
    uct₁ : (t₁ , et₁) ∈ 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₁' : ₂ℕ → G(ℕSpace ⇒ ₂Space)
    t₁' = pr₁ (pr₁ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] (t₁ , et₁) uct₁))
    et₁' : ∀(α β : ₂ℕ) → α ≣ β → pr₁ (pr₁ (t₁' α)) ≣  pr₁ (pr₁ (t₁' β))
    et₁' = pr₂ (pr₁ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] (t₁ , et₁) uct₁))
    prf₁ : (t₁' , et₁') ∈ Probe (ℕSpace ⇒ ₂Space)
    prf₁ = pr₂ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] (t₁ , et₁) 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₀ α β 0        = refl
    lemma₀ α β (succ i) = lemma₀ (α ∘ succ) (β ∘ succ) i

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

    lemma₁' : ∀(α : ₂ℕ) → ∀(φ : Map ℕSpace ₂Space)
            → pr₁ (pr₁ (t₁' (merge α (pr₁ (pr₁ φ))))) ≣ pr₁ (pr₁ φ)
    lemma₁' α φ = lemma₁ α (pr₁ (pr₁ φ))

    q : ₂ℕ → ℕ
    q = pr₁ (Exp (ℕSpace ⇒ ₂Space) ℕSpace (p , ep) (t₀ , et₀) (t₁' , et₁'))
    eq : ∀ α β → α ≣ β → q α ≡ q β
    eq = pr₂ (Exp (ℕSpace ⇒ ₂Space) ℕSpace (p , ep) (t₀ , et₀) (t₁' , et₁'))
    ucq : (q , eq) ∈ LC
    ucq = pr (t₁' , et₁') prf₁ (t₀ , et₀) uct₀

    n : ℕ
    n = pr₁ ucq

    claim : ∀ α β → α ≡[ n ] β → ∀ φ → pr₁ (pr₁ (p α)) φ ≡ pr₁ (pr₁ (p β)) φ
    claim α β en φ = claim₀ · claim₁ · claim₂ · claim₃ · claim₄
     where
      γ : ₂ℕ
      γ = pr₁ (pr₁ φ)
      en' : merge α γ ≡[ n ] merge β γ
      en' = Lemma[≡[]-≤] (lemma α β γ n en) (Lemma[n≤2n] n)
      claim₀ :  pr₁ (pr₁ (p α)) φ
              ≡ pr₁ (pr₁ (p α)) (t₁' (merge α γ))
      claim₀ = pr₂ (pr₁ (p α)) _ _ (λ i → (lemma₁ α γ i)⁻¹)
      claim₁ :  pr₁ (pr₁ (p α)) (t₁' (merge α γ))
              ≡ pr₁ (pr₁ (p (t₀ (merge α γ)))) (t₁' (merge α γ))
      claim₁ = ep _ _ (λ i → (lemma₀ α γ i)⁻¹) _
      claim₂ :  pr₁ (pr₁ (p (t₀ (merge α γ)))) (t₁' (merge α γ))
              ≡ pr₁ (pr₁ (p (t₀ (merge β γ)))) (t₁' (merge β γ))
      claim₂ = pr₁ (pr₂ ucq) (merge α γ) (merge β γ) en'
      claim₃ :  pr₁ (pr₁ (p (t₀ (merge β γ)))) (t₁' (merge β γ))
              ≡ pr₁ (pr₁ (p β)) (t₁' (merge β γ))
      claim₃ = ep _ _ (lemma₀ β γ) _
      claim₄ :  pr₁ (pr₁ (p β)) (t₁' (merge β γ))
              ≡ pr₁ (pr₁ (p β)) φ
      claim₄ = pr₂ (pr₁ (p β)) _ _ (lemma₁ β γ)

    prf : ∀(α β : ₂ℕ) → α ≡[ n ] β → ∣fan∣ (p α) ≡ ∣fan∣ (p β)
    prf α β en = ef (p α) (p β) (claim α β en)


fan-behaviour : ∀(f : Map (ℕSpace ⇒ ₂Space) ℕSpace) →
                ∀(α β : Map ℕSpace ₂Space) →
                pr₁ (pr₁ α) ≡[ pr₁ (pr₁ fan) f ] pr₁ (pr₁ β)
              → pr₁ (pr₁ f) α ≡ pr₁ (pr₁ f) β
fan-behaviour f α β en = claim₀ · claim₁ · claim₂
 where
  f' : ₂ℕ → ℕ
  f' =  pr₁ (pr₁ (Lemma[Yoneda] ℕSpace f))
  claim₀ : pr₁ (pr₁ f) α ≡ f' (pr₁ (pr₁ α))
  claim₀ = pr₂ (pr₁ f) _ _ (λ i → refl)
  claim₁ : f' (pr₁ (pr₁ α)) ≡ f' (pr₁ (pr₁ β))
  claim₁ = pr₁ (pr₂ (pr₂ (Lemma[Yoneda] ℕSpace f))) _ _ en
  claim₂ : f' (pr₁ (pr₁ β)) ≡ pr₁ (pr₁ f) β
  claim₂ = pr₂ (pr₁ f) _ _ (λ i → refl)

\end{code}