Chuangjie Xu, 2013

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

\begin{code}

module Validation-of-UC-in-LCCC where

open import MiniLibrary
open import Sequence
open import UniformContinuity
open import Inequality
open import Sequence
open import Space
open import Space-product
open import Space-exponential
open import Space-discrete
open import Space-LCC
open import Fan
open import not-not

\end{code}

The Curry-Howard interpretation of UC is the following

 ⊢ Π (f : ₂ℕ → ℕ)  Σ (n : ℕ)  Π (α β : ₂ℕ) (α ≡[n] β → f α ≡ f β).

we show that it is validated in C-spaces step by step:

(1) u₁  ::=  f : ₂ℕ → ℕ, n : ℕ, α : ₂ℕ, β : ₂ℕ ⊢ α ≡[n] β

\begin{code}

Γ⁴ : Space
Γ⁴ = ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ⊗ ℕSpace ⊗ (ℕSpace ⇒ ₂Space) ⊗ (ℕSpace ⇒ ₂Space)
πf⁴ : U Γ⁴ → U ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace)
πf⁴ (((f , _) , _) , _) = f
πn⁴ : U Γ⁴ → ℕ
πn⁴ (((_ , n) , _) , _) = n
πα⁴ : U Γ⁴ → U (ℕSpace ⇒ ₂Space)
πα⁴ (((_ , _) , α) , _) = α
πβ⁴ : U Γ⁴ → U (ℕSpace ⇒ ₂Space)
πβ⁴ (((_ , _) , _) , β) = β

Γ⁴Prp : U Γ⁴ → Set
Γ⁴Prp w = π₀(πα⁴ w) ≣[ πn⁴ w ] π₀(πβ⁴ w)

dom⟦u₁⟧ : Space
dom⟦u₁⟧ = Subspace Γ⁴ Γ⁴Prp

⟦u₁⟧ : Map dom⟦u₁⟧ Γ⁴
⟦u₁⟧ = cts-incl Γ⁴ Γ⁴Prp

\end{code}

(2) u₂  ::=  f : ₂ℕ → ℕ, n : ℕ, α : ₂ℕ, β : ₂ℕ, e : α ≡[n] β ⊢ f α ≡ f β

\begin{code}

Γ⁵ : Space
Γ⁵ = dom⟦u₁⟧
πf⁵ : U Γ⁵ → U ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace)
πf⁵ = πf⁴ ∘ π₀
πα⁵ : U Γ⁵ → U (ℕSpace ⇒ ₂Space)
πα⁵ = πα⁴ ∘ π₀
πβ⁵ : U Γ⁵ → U (ℕSpace ⇒ ₂Space)
πβ⁵ = πβ⁴ ∘ π₀

Γ⁵Prp : U Γ⁵ → Set
Γ⁵Prp w = π₀ (πf⁵ w) (πα⁵ w) ≡ π₀ (πf⁵ w) (πβ⁵ w)

dom⟦u₂⟧ : Space
dom⟦u₂⟧ = Subspace Γ⁵ Γ⁵Prp

⟦u₂⟧ : Map dom⟦u₂⟧ Γ⁵
⟦u₂⟧ = cts-incl Γ⁵ Γ⁵Prp

\end{code}

(3) u₃  ::=  f : ₂ℕ → ℕ, n : ℕ, α : ₂ℕ, β : ₂ℕ ⊢ α ≡[n] β → f α ≡ f β

\begin{code}

dom⟦u₃⟧ : Space
dom⟦u₃⟧ = dom⟪ dom⟦u₁⟧ , Γ⁴ ⟫Π[ ⟦u₁⟧ ] (dom⟦u₂⟧ , ⟦u₂⟧)

⟦u₃⟧ : Map dom⟦u₃⟧ Γ⁴
⟦u₃⟧ = π₁ (⟪ dom⟦u₁⟧ , Γ⁴ ⟫Π[ ⟦u₁⟧ ] (dom⟦u₂⟧ , ⟦u₂⟧))

\end{code}

(4) u₄' ::=  f : ₂ℕ → ℕ, n : ℕ, α : ₂ℕ, ⊢ ₂ℕ

    u₄  ::=  f : ₂ℕ → ℕ, n : ℕ, α : ₂ℕ, ⊢ Π (β : ₂ℕ) (α ≡[n] β → f α ≡ f β)

\begin{code}

Γ³ : Space
Γ³ = ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ⊗ ℕSpace ⊗ (ℕSpace ⇒ ₂Space)

⟦u₄'⟧ : Map Γ⁴ Γ³
⟦u₄'⟧ = continuous-π₀ {Γ³} {ℕSpace ⇒ ₂Space}

dom⟦u₄⟧ : Space
dom⟦u₄⟧ = dom⟪ Γ⁴ , Γ³ ⟫Π[ ⟦u₄'⟧ ] (dom⟦u₃⟧ , ⟦u₃⟧)

⟦u₄⟧ : Map dom⟦u₄⟧ Γ³
⟦u₄⟧ = π₁ (⟪ Γ⁴ , Γ³ ⟫Π[ ⟦u₄'⟧ ] (dom⟦u₃⟧ , ⟦u₃⟧))

\end{code}

(5) u₅' ::=  f : ₂ℕ → ℕ, n : ℕ ⊢ ₂ℕ

    u₅  ::=  f : ₂ℕ → ℕ, n : ℕ ⊢ Π(α : ₂ℕ)  Π(β : ₂ℕ) (α ≡[n] β → f α ≡ f β)

\begin{code}

Γ² : Space
Γ² = ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ⊗ ℕSpace

⟦u₅'⟧ : Map Γ³ Γ²
⟦u₅'⟧ = continuous-π₀ {Γ²} {ℕSpace ⇒ ₂Space}

dom⟦u₅⟧ : Space
dom⟦u₅⟧ = dom⟪ Γ³ , Γ² ⟫Π[ ⟦u₅'⟧ ] (dom⟦u₄⟧ , ⟦u₄⟧)

⟦u₅⟧ : Map dom⟦u₅⟧ Γ²
⟦u₅⟧ = π₁ (⟪ Γ³ , Γ² ⟫Π[ ⟦u₅'⟧ ] (dom⟦u₄⟧ , ⟦u₄⟧))

\end{code}

(6) u₆' ::=  f : ₂ℕ → ℕ ⊢ ℕ

    u₆  ::=  f : ₂ℕ → ℕ ⊢ Σ (n : ℕ)  Π(α : ₂ℕ)  Π(β : ₂ℕ) (α ≡[n] β → f α ≡ f β)

\begin{code}

Γ¹ : Space
Γ¹ = (ℕSpace ⇒ ₂Space) ⇒ ℕSpace

⟦u₆'⟧ : Map Γ² Γ¹
⟦u₆'⟧ = continuous-π₀ {Γ¹} {ℕSpace}

dom⟦u₆⟧ : Space
dom⟦u₆⟧ = dom⟪ Γ² , Γ¹ ⟫Σ[ ⟦u₆'⟧ ] (dom⟦u₅⟧ , ⟦u₅⟧)

⟦u₆⟧ : Map dom⟦u₆⟧ Γ¹
⟦u₆⟧ = π₁ (⟪ Γ² , Γ¹ ⟫Σ[ ⟦u₆'⟧ ] (dom⟦u₅⟧ , ⟦u₅⟧))

\end{code}

(7) uc  ::=  ⊢ Π (f : ₂ℕ → ℕ)  Σ (n : ℕ)  Π (α β : ₂ℕ) (α ≡[n] β → f α ≡ f β).

\begin{code}

Γ⁰ : Space
Γ⁰ = ⒈Space

dom⟦uc⟧ : Space
dom⟦uc⟧ = dom⟪ Γ¹ , Γ⁰ ⟫Π[ continuous-unit {Γ¹} ] (dom⟦u₆⟧ , ⟦u₆⟧)

\end{code}

The Space dom⟦uc⟧ is inhabited. One inhabitant is the following, which
is defined using the fan functional.

\begin{code}

uc : U dom⟦uc⟧
uc = (⋆ , h , cts) , (λ _ → refl)
 where
  dom-h : Space
  dom-h = Subspace ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) (λ _ → [ ⋆ ≡ ⋆ ])
       -- ⟪ Γ¹ , Γ⁰ ⟫ (continuous-unit {Γ¹}) ⁻¹₍ ⋆ ₎
  cod-h : Space
  cod-h = Subspace dom⟦u₅⟧ (λ _ → [ ⋆ ≡ ⋆ ])
       -- ⟪ dom⟦u₆⟧ , Γ⁰ ⟫ (⟪ dom⟦u₆⟧ , Γ¹ , Γ⁰ ⟫ (continuous-unit {Γ¹}) ○ ⟦u₆⟧) ⁻¹₍ ⋆ ₎
  h : U dom-h → U cod-h
  h (f , _) = (((f , π₀ fan f) , h₁ , cts₁) , (λ _ → refl)) , hide refl
   where
    dom-h₁ : Space
    dom-h₁ = Subspace Γ³ (λ w → [ π₀ w ≡ (f , π₀ fan f) ])
          -- ⟪ Γ³ , Γ² ⟫ ⟦u₅'⟧ ⁻¹₍ (f , π₀ fan f) ₎
    cod-h₁ : Space
    cod-h₁ = Subspace dom⟦u₄⟧ (λ w → [ π₀ (π₀ ⟦u₄⟧ w) ≡ (f , π₀ fan f) ])
          -- ⟪ dom⟦u₄⟧ , Γ² ⟫ ⟪ dom⟦u₄⟧ , Γ³ , Γ² ⟫ ⟦u₅'⟧ ○ ⟦u₄⟧ ⁻¹₍ (f , π₀ fan f) ₎
    h₁ : U dom-h₁ → U cod-h₁
    h₁ (((f₁ , n₁) , α) , e₁) = (((((f₁ , n₁) , α)) , h₂ , cts₂) , (λ _ → refl)) , e₁
     where
      dom-h₂ : Space
      dom-h₂ = Subspace Γ⁴ (λ w → [ π₀ w ≡ ((f₁ , n₁) , α) ])
            -- ⟪ Γ⁴ , Γ³ ⟫ ⟦u₄'⟧ ⁻¹₍ ((f₁ , n₁) , α) ₎
      cod-h₂ : Space
      cod-h₂ = Subspace dom⟦u₃⟧ (λ w → [ π₀ (π₀ ⟦u₃⟧ w) ≡ ((f₁ , n₁) , α) ])
            -- ⟪ dom⟦u₃⟧ , Γ³ ⟫ ⟪ dom⟦u₃⟧ , Γ⁴ , Γ³ ⟫ ⟦u₄'⟧ ○ ⟦u₃⟧ ⁻¹₍ ((f₁ , n₁) , α) ₎
      h₂ : U dom-h₂ → U cod-h₂
      h₂ ((((f₂ , n₂) , α₂) , β) , e₂) = (((((f₂ , n₂) , α₂) , β) , h₃ , cts₃) , (λ _ → refl)) , e₂
       where
        dom-h₃ : Space
        dom-h₃ = Subspace dom⟦u₁⟧ (λ w → [ π₀ w ≡ (((f₂ , n₂) , α₂) , β) ])
              -- ⟪ dom⟦u₁⟧ , Γ⁴ ⟫ ⟦u₁⟧ ⁻¹₍ (((f₂ , n₂) , α₂) , β) ₎
        cod-h₃ : Space
        cod-h₃ = Subspace dom⟦u₂⟧ (λ w → [ π₀ (π₀ w) ≡ (((f₂ , n₂) , α₂) , β) ])
              -- ⟪ dom⟦u₂⟧ , Γ⁴ ⟫ ⟪ dom⟦u₂⟧ , dom⟦u₁⟧ , Γ⁴ ⟫ ⟦u₁⟧ ○ ⟦u₂⟧ ⁻¹₍ (((f₂ , n₂) , α₂) , β) ₎
        h₃ : U dom-h₃ → U cod-h₃
        h₃ (((((f₃ , n₃) , α₃) , β₃) , en₃) , e₃) = (((((f₃ , n₃) , α₃) , β₃) , en₃) , goal) , e₃
         where
{-
          e₁ : [ (f₁ , n₁) ≡ (f , π₀ fan f) ]
          e₂ : [ ((f₂ , n₂) , α₂) ≡ ((f₁ , n₁) , α) ]
          e₃ : [ (((f₃ , n₃) , α₃) , β₃) ≡ (((f₂ , n₂) , α₂) , β) ]
-}
          eq₃₂ : [ (f₃ , n₃) ≡ (f₂ , n₂) ]
          eq₃₂ = [ap] (π₀ ∘ π₀) e₃
          eq₂₁ : [ (f₂ , n₂) ≡ (f₁ , n₁) ]
          eq₂₁ = [ap] π₀ e₂
          eq₃₀ : [ (f₃ , n₃) ≡ (f , π₀ fan f) ]
          eq₃₀ = [trans] eq₃₂ ([trans] eq₂₁ e₁)
          eqf : [ f₃ ≡ f ]
          eqf = [ap] π₀ eq₃₀
          eqn : [ n₃ ≡ π₀ fan f ]
          eqn = [ap] π₁ eq₃₀
          [eqn₃] : [ n₃ ≡ π₀ fan f₃ ]
          [eqn₃] = [transport] {Map (ℕSpace ⇒ ₂Space) ℕSpace} {λ x → n₃ ≡ π₀ fan x} ([sym] eqf) eqn
          eqn₃ : n₃ ≡ π₀ fan f₃
          eqn₃ = Lemma[[≡]→≡]-ℕ [eqn₃]
          en₃' : π₀ α₃ ≣[ π₀ fan f₃ ] π₀ β₃
          en₃' = transport {ℕ} {λ x → π₀ α₃ ≣[ x ] π₀ β₃} eqn₃ en₃
          goal : π₀ f₃ α₃ ≡ π₀ f₃ β₃
          goal = fan-behaviour f₃ α₃ β₃ en₃'
                 -------------
        cts₃ : continuous {dom-h₃} {cod-h₃} h₃
            -- ∀(p : ₂ℕ → U dom-h₃) → π₀ ∘ π₀ ∘ p ∈ Probe Γ⁴ → π₀ ∘ π₀ ∘ π₀ ∘ h₃ ∘ p ∈ Probe Γ⁴
        cts₃ _ pP = pP

      cts₂ : continuous {dom-h₂} {cod-h₂} h₂
          -- ∀(p : ₂ℕ → U dom-h₂) → π₀ ∘ p ∈ Probe Γ⁴ → π₀ ∘ h₂ ∘ p ∈ Probe dom⟦u₃⟧
      cts₂ _ pP = ∧-intro pP (λ _ _ _ qQ _ → qQ)

    cts₁ : continuous {dom-h₁} {cod-h₁} h₁
        -- ∀(p : ₂ℕ → U dom-h₁) → π₀ ∘ p ∈ Probe Γ³ → π₀ ∘ h₁ ∘ p ∈ Probe dom⟦u₄⟧
    cts₁ _ pP = ∧-intro pP (λ _ _ _ qQ _ → ∧-intro qQ (λ _ _ _ rR _ → rR))

  cts : ∀(p : ₂ℕ → U dom-h) → π₀ ∘ p ∈ Probe ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) → π₀ ∘ h ∘ p ∈ Probe dom⟦u₅⟧
     -- continuous {dom-h} {cod-h} h
  cts p pP = ∧-intro (∧-intro pP (π₁ fan (π₀ ∘ p) pP))
                     (λ _ _ _ qQ _ → ∧-intro qQ (λ _ _ _ rR _ → ∧-intro rR (λ _ _ _ sS _ → sS)))

\end{code}

To validate UC, it is equivalent to show that the space dom⟦uc⟧ is
inhabited.

\begin{code}

UC-is-validated : Set
UC-is-validated = U dom⟦uc⟧

Theorem : UC-is-validated
Theorem = uc

\end{code}