Chuangjie Xu 2013

(Improved on 14 August, 2014)

\begin{code}

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

module UsingFunext.ModellingUC.Hierarchy where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingFunext.Funext
open import UsingFunext.Space.Coverage
open import UsingFunext.Space.Space
open import UsingFunext.Space.DiscreteSpace
open import UsingFunext.Space.CartesianClosedness
open import UsingFunext.Space.IndiscreteSpace

\end{code}

Type structure

\begin{code}

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

\end{code}

The full type hierarchy (FTH) is a full subcategory of sets. Objects in FTH can
be considered as (the interpretations of) the elements of Ty, while morphisms
are maps ⟦ σ ⟧s → ⟦ τ ⟧s, where ⟦_⟧s is the interpretation of Ty in Set.

\begin{code}

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

\end{code}

Similarly, the Kleene-Kreisel hierarchy (KKH), via C-space manifestation, also
contains (interpretations of) elements of Ty as objects, and continuous maps
from ⟦ σ ⟧c to ⟦ τ ⟧c as morphisms.

\begin{code}

⟦_⟧c : Ty → 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. Hence 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}

Lemma[simple-probe-hprop] : (σ : Ty) → (p : ₂ℕ → U ⟦ σ ⟧c)
                          → ∀(pσ₀ pσ₁ : p ∈ Probe ⟦ σ ⟧c) → pσ₀ ≡ pσ₁
Lemma[simple-probe-hprop] Ⓝ p pN₀ pN₁ = Lemma[LC-hprop] ℕ-hset p pN₀ pN₁
Lemma[simple-probe-hprop] (σ ⊠ τ) r rστ₀ rστ₁ = pairˣ⁼ IHσ IHτ
 where
  IHσ : pr₁ rστ₀ ≡ pr₁ rστ₁
  IHσ = Lemma[simple-probe-hprop] σ (pr₁ ∘ r) (pr₁ rστ₀) (pr₁ rστ₁)
  IHτ : pr₂ rστ₀ ≡ pr₂ rστ₁
  IHτ = Lemma[simple-probe-hprop] τ (pr₂ ∘ r) (pr₂ rστ₀) (pr₂ rστ₁)
Lemma[simple-probe-hprop] (σ ⇨ τ) 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[simple-probe-hprop] τ (λ α → (pr₁ ∘ r)(t α)(p α))
                                           (rστ₀ p pσ t uc) (rστ₁ p pσ t uc)
  goal : rστ₀ ≡ rστ₁
  goal = funext⁴ IH
        ---------

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

\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}

Lemma[UC-implies-indiscreteness] : Axiom[UC-ℕ] → ∀(σ : Ty) → indiscrete ⟦ σ ⟧c
Lemma[UC-implies-indiscreteness] ucN Ⓝ = ucN
Lemma[UC-implies-indiscreteness] ucN (σ ⊠ τ) = λ p → IHσ (pr₁ ∘ p) , IHτ (pr₂ ∘ 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τ (λ α → pr₁(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,
in the sense that the two interpretations of each type are equivalent.

\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→⟦σ⟧s≅⟦σ⟧c] : Axiom[UC-ℕ] → ∀(σ : Ty) → ⟦ σ ⟧s ≅ U ⟦ σ ⟧c
Theorem[UC→⟦σ⟧s≅⟦σ⟧c] ucN Ⓝ = id , id , (λ x → refl) , (λ y → refl)
Theorem[UC→⟦σ⟧s≅⟦σ⟧c] ucN (σ ⊠ τ) = f , g , ex , ey
 where
  IHσ : ⟦ σ ⟧s ≅ U ⟦ σ ⟧c
  IHσ = Theorem[UC→⟦σ⟧s≅⟦σ⟧c] ucN σ
  fσ  : ⟦ σ ⟧s → U ⟦ σ ⟧c
  fσ  = pr₁ IHσ
  gσ  : U ⟦ σ ⟧c → ⟦ σ ⟧s
  gσ  = pr₁ (pr₂ IHσ)
  exσ : ∀(x : ⟦ σ ⟧s)   → gσ(fσ x) ≡ x
  exσ = pr₁ (pr₂ (pr₂ IHσ))
  eyσ : ∀(y : U ⟦ σ ⟧c) → fσ(gσ y) ≡ y
  eyσ = pr₂ (pr₂ (pr₂ IHσ))
  IHτ : ⟦ τ ⟧s ≅ U ⟦ τ ⟧c
  IHτ = Theorem[UC→⟦σ⟧s≅⟦σ⟧c] ucN τ
  fτ  : ⟦ τ ⟧s → U ⟦ τ ⟧c
  fτ  = pr₁ IHτ
  gτ  : U ⟦ τ ⟧c → ⟦ τ ⟧s
  gτ  = pr₁ (pr₂ IHτ)
  exτ : ∀(x : ⟦ τ ⟧s)   → gτ(fτ x) ≡ x
  exτ = pr₁ (pr₂ (pr₂ IHτ))
  eyτ : ∀(y : U ⟦ τ ⟧c) → fτ(gτ y) ≡ y
  eyτ = pr₂ (pr₂ (pr₂ 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') = pairˣ⁼ (exσ x) (exτ x')
  ey : ∀(y : U ⟦ σ ⟧c × U ⟦ τ ⟧c) → f(g y) ≡ y
  ey (y , y') = pairˣ⁼ (eyσ y) (eyτ y')
Theorem[UC→⟦σ⟧s≅⟦σ⟧c] ucN (σ ⇨ τ) = f , g , ex , ey
 where
  IHσ : ⟦ σ ⟧s ≅ U ⟦ σ ⟧c
  IHσ = Theorem[UC→⟦σ⟧s≅⟦σ⟧c] ucN σ
  fσ  : ⟦ σ ⟧s → U ⟦ σ ⟧c
  fσ  = pr₁ IHσ
  gσ  : U ⟦ σ ⟧c → ⟦ σ ⟧s
  gσ  = pr₁ (pr₂ IHσ)
  exσ : ∀(x : ⟦ σ ⟧s)   → gσ(fσ x) ≡ x
  exσ = pr₁ (pr₂ (pr₂ IHσ))
  eyσ : ∀(y : U ⟦ σ ⟧c) → fσ(gσ y) ≡ y
  eyσ = pr₂ (pr₂ (pr₂ IHσ))
  IHτ : ⟦ τ ⟧s ≅ U ⟦ τ ⟧c
  IHτ = Theorem[UC→⟦σ⟧s≅⟦σ⟧c] ucN τ
  fτ  : ⟦ τ ⟧s → U ⟦ τ ⟧c
  fτ  = pr₁ IHτ
  gτ  : U ⟦ τ ⟧c → ⟦ τ ⟧s
  gτ  = pr₁ (pr₂ IHτ)
  exτ : ∀(x : ⟦ τ ⟧s)   → gτ(fτ x) ≡ x
  exτ = pr₁ (pr₂ (pr₂ IHτ))
  eyτ : ∀(y : U ⟦ τ ⟧c) → fτ(gτ y) ≡ y
  eyτ = pr₂ (pr₂ (pr₂ 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 = 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[simple-Map-≡] ⟦ σ ⟧c τ (f(g ψ)) ψ claim
   where
    claim : ∀(y : U ⟦ σ ⟧c) → pr₁ (f (g ψ)) y ≡ pr₁ ψ y
    claim y = e₀ · e₁
     where
      e₀ : fτ(gτ(pr₁ ψ (fσ(gσ y)))) ≡ fτ(gτ(pr₁ ψ y))
      e₀ = ap (fτ ∘ gτ ∘ (pr₁ ψ)) (eyσ y)
      e₁ : fτ(gτ(pr₁ ψ y)) ≡ pr₁ ψ y
      e₁ = eyτ (pr₁ ψ y)

\end{code}

Since we consider objects in both hierarchies as elements of Ty, the equivalence
on objects is simply the identity.  Then the equivalence on hom-sets directly
follows the above theorem.

\begin{code}

HomFTH : Ty → Ty → Set
HomFTH σ τ = ⟦ σ ⟧s → ⟦ τ ⟧s

HomKKH : Ty → Ty → Set
HomKKH σ τ = Map ⟦ σ ⟧c ⟦ τ ⟧c

Corollary[UC→HomFTH≅HomKKH] : Axiom[UC-ℕ] → ∀(σ τ : Ty) → HomFTH σ τ ≅ HomKKH σ τ
Corollary[UC→HomFTH≅HomKKH] uc σ τ = Theorem[UC→⟦σ⟧s≅⟦σ⟧c] uc (σ ⇨ τ)

\end{code}