Chuangjie Xu, 2013

This corresponds to Section 3.2 of the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

\begin{code}

module Hierarchy where

open import MiniLibrary
open import Inequality
open import Sequence
open import UniformContinuity
open import Space
open import Space-product
open import Space-coproduct
open import Space-exponential
open import Space-discrete

\end{code}

If all maps ₂ℕ → ℕ are uniformly continuous, then so are all ₂ℕ → ₂.

\begin{code}

UC-② : Set
UC-② = ∀(p : ₂ℕ → ₂) → locally-constant p

UC-Ⓝ : Set
UC-Ⓝ = ∀(p : ₂ℕ → ℕ) → locally-constant p

UC-Ⓝ-to-UC-② : UC-Ⓝ → UC-②
UC-Ⓝ-to-UC-② ucN p = Lemma[LM-₂-least-modulus] p n pr2
 where
  ₂-ℕ : ₂ → ℕ
  ₂-ℕ ₀ = 
  ₂-ℕ ₁ = 
  lemma : ∀(b b' : ₂) → ₂-ℕ b ≡ ₂-ℕ b' → b ≡ b'
  lemma ₀ ₀ refl = refl
  lemma ₀ ₁ ()
  lemma ₁ ₀ ()
  lemma ₁ ₁ refl = refl
  n : ℕ
  n = ∃-witness (ucN (₂-ℕ ∘ p))
  prN : ∀(α β : ₂ℕ) → α ≣[ n ] β → ₂-ℕ(p α) ≡ ₂-ℕ(p β)
  prN = ∧-elim₀ (∃-elim (ucN (₂-ℕ ∘ p)))
  pr2 : ∀(α β : ₂ℕ) → α ≣[ n ] β → p α ≡ p β
  pr2 α β en = lemma (p α) (p β) (prN α β en)

\end{code}

Type hierarchy:

\begin{code}

data Ty : Set where
 ② : Ty
 Ⓝ : Ty
 _⊠_ : Ty → Ty → Ty
 _⇨_ : Ty → Ty → Ty

\end{code}

The full type hierarchy:

\begin{code}

⟦_⟧s : Ty → Set
⟦ ② ⟧s = ₂
⟦ Ⓝ ⟧s = ℕ
⟦ σ ⊠ τ ⟧s = ⟦ σ ⟧s × ⟦ τ ⟧s
⟦ σ ⇨ τ ⟧s = ⟦ σ ⟧s → ⟦ τ ⟧s

\end{code}

The Kleene-Kreisel hierarchy, via C-space manifestation:

\begin{code}

⟦_⟧c : Ty → Space
⟦ ② ⟧c = ₂Space
⟦ Ⓝ ⟧c = ℕSpace
⟦ σ ⊠ τ ⟧c = ⟦ σ ⟧c ⊗ ⟦ τ ⟧c
⟦ σ ⇨ τ ⟧c = ⟦ σ ⟧c ⇒ ⟦ τ ⟧c

\end{code}

In this module, the double negation of function extensionality doesn't
seem to be sufficient. Hense we use the full one as a hypothesis, to
show the following:

(1) Probes on the spaces in the Kleene-Kreisel hierarchy are
    hpropositions.

(2) If two continuous maps in the Kleene-Kreisel hierarchy are
    pointwise equal, the they are identical morphisms.

\begin{code}

open import not-not-funext

Lemma[LC-hprop]' : Funext → {X : Set} → hset X → ∀(p : ₂ℕ → X) → (lc₀ lc₁ : LC p) → lc₀ ≡ lc₁
Lemma[LC-hprop]' funext hsX p (n₀ , (pr₀ , min₀)) (n₁ , (pr₁ , min₁)) = Lemma[≡-Σ] e ee
 where
  e : n₀ ≡ n₁
  e = Lemma[m≤n∧n≤m→m=n] (min₀ n₁ pr₁) (min₁ n₀ pr₀)
  pr₀'min₀' :  (∀(α β : ₂ℕ) → α ≣[ n₁ ] β → p α ≡ p β)
             ∧ (∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≣[ n' ] β → p α ≡ p β) → n₁ ≤ n')
  pr₀'min₀' = transport e (∧-intro pr₀ min₀)
  pr₀' : ∀(α β : ₂ℕ) → α ≣[ n₁ ] β → p α ≡ p β
  pr₀' α β en = ∧-elim₀ pr₀'min₀' α β en
  eepr : ∀(α β : ₂ℕ) → (en : α ≣[ n₁ ] β) → pr₀' α β en ≡ pr₁ α β en
  eepr α β en = hsX (p α) (p β) (pr₀' α β en) (pr₁ α β en)
  epr : pr₀' ≡ pr₁
  epr = funext (λ α → funext (λ β → funext (λ en → eepr α β en)))
  min₀' : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≣[ n' ] β → p α ≡ p β) → n₁ ≤ n'
  min₀' = ∧-elim₁ pr₀'min₀'
  eemin : ∀(n' : ℕ) → (pr' : ∀(α β : ₂ℕ) → α ≣[ n' ] β → p α ≡ p β) → min₀' n' pr' ≡ min₁ n' pr'
  eemin n' pr' = Lemma[≤-hprop] (min₀' n' pr') (min₁ n' pr')
  emin : min₀' ≡ min₁
  emin = funext (λ n' → funext (λ pr' → eemin n' pr'))
  ee : (pr₀' , min₀') ≡ (pr₁ , min₁)
  ee = Lemma[≡-∧] epr emin

Lemma[probe-hprop] : Funext → (σ : Ty) → (p : ₂ℕ → U ⟦ σ ⟧c) → (pσ₀ pσ₁ : p ∈ Probe ⟦ σ ⟧c) → pσ₀ ≡ pσ₁
Lemma[probe-hprop] funext ② p p2₀ p2₁ = Lemma[LC-hprop]' funext ₂-hset p p2₀ p2₁
Lemma[probe-hprop] funext Ⓝ p pN₀ pN₁ = Lemma[LC-hprop]' funext ℕ-hset p pN₀ pN₁
Lemma[probe-hprop] funext (σ ⊠ τ) r rστ₀ rστ₁ = Lemma[≡-∧] IHσ IHτ
 where
  IHσ : π₀ rστ₀ ≡ π₀ rστ₁
  IHσ = Lemma[probe-hprop] funext σ (π₀ ∘ r) (π₀ rστ₀) (π₀ rστ₁)
  IHτ : π₁ rστ₀ ≡ π₁ rστ₁
  IHτ = Lemma[probe-hprop] funext τ (π₁ ∘ r) (π₁ rστ₀) (π₁ rστ₁)
Lemma[probe-hprop] funext (σ ⇨ τ) r rστ₀ rστ₁ = goal
 where
  IH : ∀(p : ₂ℕ → U ⟦ σ ⟧c) → (pσ : p ∈ Probe ⟦ σ ⟧c) → ∀(t : ₂ℕ → ₂ℕ) → (uc : t ∈ C) →
       rστ₀ p pσ t uc ≡ rστ₁ p pσ t uc
  IH p pσ t uc = Lemma[probe-hprop] funext τ (λ α → (π₀ ∘ r)(t α)(p α)) (rστ₀ p pσ t uc)
                                                                        (rστ₁ p pσ t uc)
  goal : rστ₀ ≡ rστ₁
  goal = funext (λ p → funext (λ pσ → funext (λ t → funext (λ uc → IH p pσ t uc))))

Lemma[≡-Map] : Funext → ∀(X : Space) → ∀(σ : Ty) → ∀(f g : Map X ⟦ σ ⟧c) →
               (∀(x : U X) → π₀ f x ≡ π₀ g x) → f ≡ g
Lemma[≡-Map] funext X σ (f , cf) (g , cg) ex = Lemma[≡-Σ] e₀ e₁
 where
  e₀ : f ≡ g
  e₀ = funext ex
  cg' : continuous {X} {⟦ σ ⟧c} g
  cg' = transport {U X → U ⟦ σ ⟧c} {continuous {X} {⟦ σ ⟧c}} e₀ cf
  ee₁ : ∀(p : ₂ℕ → U X) → (pX : p ∈ Probe X) → cg' p pX ≡ cg p pX
  ee₁ p pX = Lemma[probe-hprop] funext σ (g ∘ p) (cg' p pX) (cg p pX)
  e₁ : cg' ≡ cg
  e₁ = funext (λ p → funext (λ pX → ee₁ p pX))

\end{code}

The main lemma says that if UC holds then all spaces in the
Kleene-Kreisel hierarchy are indiscrete, in the sense that all maps
from cantor space are probes.

Notice that this doesn't depend on function extensionality.

\begin{code}

indiscrete : Space → Set
indiscrete X = ∀(p : ₂ℕ → U X) → p ∈ Probe X

Lemma[UC-implies-indiscreteness] : UC-Ⓝ → ∀(σ : Ty) → indiscrete ⟦ σ ⟧c
Lemma[UC-implies-indiscreteness] ucN ② = UC-Ⓝ-to-UC-② ucN
Lemma[UC-implies-indiscreteness] ucN Ⓝ = ucN
Lemma[UC-implies-indiscreteness] ucN (σ ⊠ τ) = λ p → IHσ (π₀ ∘ p) , IHτ (π₁ ∘ p)
 where
  IHσ : indiscrete ⟦ σ ⟧c
  IHσ = Lemma[UC-implies-indiscreteness] ucN σ
  IHτ : indiscrete ⟦ τ ⟧c
  IHτ = Lemma[UC-implies-indiscreteness] ucN τ
Lemma[UC-implies-indiscreteness] ucN (σ ⇨ τ) = λ r p _ t _ → IHτ (λ α → π₀(r(t α))(p α))
 where
  IHτ : indiscrete ⟦ τ ⟧c
  IHτ = Lemma[UC-implies-indiscreteness] ucN τ

\end{code}

If UC holds for types, then the full type and Kleene-Kreisel
hierarchies agree.

\begin{code}

_≅_ : Set → Set → Set
X ≅ Y = ∃ \(f : X → Y) → ∃ \(g : Y → X) →
           (∀(x : X) → g(f x) ≡ x) ∧ (∀(y : Y) → f(g y) ≡ y)

Theorem[UC-KK-full] : Funext → UC-Ⓝ → ∀(σ : Ty) → ⟦ σ ⟧s ≅ U ⟦ σ ⟧c
Theorem[UC-KK-full] funext ucN ② = id , id , (λ x → refl) , (λ y → refl)
Theorem[UC-KK-full] funext ucN Ⓝ = id , id , (λ x → refl) , (λ y → refl)
Theorem[UC-KK-full] funext ucN (σ ⊠ τ) = f , g , ex , ey
 where
  IHσ : ⟦ σ ⟧s ≅ U ⟦ σ ⟧c
  IHσ = Theorem[UC-KK-full] funext ucN σ
  fσ : ⟦ σ ⟧s → U ⟦ σ ⟧c
  fσ = π₀ IHσ
  gσ : U ⟦ σ ⟧c → ⟦ σ ⟧s
  gσ = π₀ (π₁ IHσ)
  exσ : ∀(x : ⟦ σ ⟧s)   → gσ(fσ x) ≡ x
  exσ = π₀ (π₁ (π₁ IHσ))
  eyσ : ∀(y : U ⟦ σ ⟧c) → fσ(gσ y) ≡ y
  eyσ = π₁ (π₁ (π₁ IHσ))
  IHτ : ⟦ τ ⟧s ≅ U ⟦ τ ⟧c
  IHτ = Theorem[UC-KK-full] funext ucN τ
  fτ : ⟦ τ ⟧s → U ⟦ τ ⟧c
  fτ = π₀ IHτ
  gτ : U ⟦ τ ⟧c → ⟦ τ ⟧s
  gτ = π₀ (π₁ IHτ)
  exτ : ∀(x : ⟦ τ ⟧s)   → gτ(fτ x) ≡ x
  exτ = π₀ (π₁ (π₁ IHτ))
  eyτ : ∀(y : U ⟦ τ ⟧c) → fτ(gτ y) ≡ y
  eyτ = π₁ (π₁ (π₁ IHτ))
  f : ⟦ σ ⟧s × ⟦ τ ⟧s → U ⟦ σ ⟧c × U ⟦ τ ⟧c
  f (x , x') = (fσ x , fτ x')
  g : U ⟦ σ ⟧c × U ⟦ τ ⟧c → ⟦ σ ⟧s × ⟦ τ ⟧s
  g (y , y') = (gσ y , gτ y')
  ex : ∀(x : ⟦ σ ⟧s × ⟦ τ ⟧s) → g(f x) ≡ x
  ex (x , x') = Lemma[≡-∧] (exσ x) (exτ x')
  ey : ∀(y : U ⟦ σ ⟧c × U ⟦ τ ⟧c) → f(g y) ≡ y
  ey (y , y') = Lemma[≡-∧] (eyσ y) (eyτ y')
Theorem[UC-KK-full] funext ucN (σ ⇨ τ) = f , g , ex , ey
 where
  IHσ : ⟦ σ ⟧s ≅ U ⟦ σ ⟧c
  IHσ = Theorem[UC-KK-full] funext ucN σ
  fσ : ⟦ σ ⟧s → U ⟦ σ ⟧c
  fσ = π₀ IHσ
  gσ : U ⟦ σ ⟧c → ⟦ σ ⟧s
  gσ = π₀ (π₁ IHσ)
  exσ : ∀(x : ⟦ σ ⟧s)   → gσ(fσ x) ≡ x
  exσ = π₀ (π₁ (π₁ IHσ))
  eyσ : ∀(y : U ⟦ σ ⟧c) → fσ(gσ y) ≡ y
  eyσ = π₁ (π₁ (π₁ IHσ))
  IHτ : ⟦ τ ⟧s ≅ U ⟦ τ ⟧c
  IHτ = Theorem[UC-KK-full] funext ucN τ
  fτ : ⟦ τ ⟧s → U ⟦ τ ⟧c
  fτ = π₀ IHτ
  gτ : U ⟦ τ ⟧c → ⟦ τ ⟧s
  gτ = π₀ (π₁ IHτ)
  exτ : ∀(x : ⟦ τ ⟧s)   → gτ(fτ x) ≡ x
  exτ = π₀ (π₁ (π₁ IHτ))
  eyτ : ∀(y : U ⟦ τ ⟧c) → fτ(gτ y) ≡ y
  eyτ = π₁ (π₁ (π₁ IHτ))
  f : (⟦ σ ⟧s → ⟦ τ ⟧s) → U(⟦ σ ⟧c ⇒ ⟦ τ ⟧c)
  f φ = fτ ∘ φ ∘ gσ , λ p _ → Lemma[UC-implies-indiscreteness] ucN τ (fτ ∘ φ ∘ gσ ∘ p)
  g : U(⟦ σ ⟧c ⇒ ⟦ τ ⟧c) → ⟦ σ ⟧s → ⟦ τ ⟧s
  g (ψ , _) = gτ ∘ ψ ∘ fσ
  ex : ∀(φ : ⟦ σ ⟧s → ⟦ τ ⟧s) → g(f φ) ≡ φ
  ex φ = funext claim
   where
    claim : ∀(x : ⟦ σ ⟧s) → g (f φ) x ≡ φ x
    claim x = trans e₀ e₁
     where
      e₀ : gτ(fτ(φ(gσ(fσ x)))) ≡ gτ(fτ(φ x))
      e₀ = ap (gτ ∘ fτ ∘ φ) (exσ x)
      e₁ : gτ(fτ(φ x)) ≡ φ x
      e₁ = exτ (φ x)
  ey : ∀(ψ : U(⟦ σ ⟧c ⇒ ⟦ τ ⟧c)) → f(g ψ) ≡ ψ
  ey ψ = Lemma[≡-Map] funext ⟦ σ ⟧c τ (f(g ψ)) ψ claim
   where
    claim : ∀(y : U ⟦ σ ⟧c) → π₀ (f (g ψ)) y ≡ π₀ ψ y
    claim y = trans e₀ e₁
     where
      e₀ : fτ(gτ(π₀ ψ (fσ(gσ y)))) ≡ fτ(gτ(π₀ ψ y))
      e₀ = ap (fτ ∘ gτ ∘ (π₀ ψ)) (eyσ y)
      e₁ : fτ(gτ(π₀ ψ y)) ≡ π₀ ψ y
      e₁ = eyτ (π₀ ψ y)

\end{code}