Chuangjie Xu 2013

\begin{code}

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

module UsingFunext.ModellingUC.ValidatingUCviaLCCC 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.Space.Coverage
open import UsingFunext.Space.Space
open import UsingFunext.Space.DiscreteSpace
open import UsingFunext.Space.CartesianClosedness
open import UsingFunext.Space.LocalCartesianClosedness
open import UsingFunext.Space.Fan

\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 = pr₁(πα⁴ w) ≡[ πn⁴ w ] pr₁(πβ⁴ 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⁴ ∘ pr₁
πα⁵ : U Γ⁵ → U (ℕSpace ⇒ ₂Space)
πα⁵ = πα⁴ ∘ pr₁
πβ⁵ : U Γ⁵ → U (ℕSpace ⇒ ₂Space)
πβ⁵ = πβ⁴ ∘ pr₁

Γ⁵Prp : U Γ⁵ → Set
Γ⁵Prp w = pr₁ (πf⁵ w) (πα⁵ w) ≡ pr₁ (π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₃⟧ = pr₂ (⟪ 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₄'⟧ = cpr₁ Γ³ (ℕSpace ⇒ ₂Space)

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

⟦u₄⟧ : Map dom⟦u₄⟧ Γ³
⟦u₄⟧ = pr₂ (⟪ Γ⁴ , Γ³ ⟫Π[ ⟦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₅'⟧ = cpr₁ Γ² (ℕSpace ⇒ ₂Space)

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

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

\end{code}

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

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

\begin{code}

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

⟦u₆'⟧ : Map Γ² Γ¹
⟦u₆'⟧ = cpr₁ Γ¹ ℕSpace

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

⟦u₆⟧ : Map dom⟦u₆⟧ Γ¹
⟦u₆⟧ = pr₂ (⟪ Γ² , Γ¹ ⟫Σ[ ⟦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 , pr₁ fan f) , h₁ , cts₁) , (λ _ → refl)) , refl
   where
    dom-h₁ : Space
    dom-h₁ = Subspace Γ³ (λ w → pr₁ w ≡ (f , pr₁ fan f))
          -- ⟪ Γ³ , Γ² ⟫ ⟦u₅'⟧ ⁻¹₍ (f , pr₁ fan f) ₎
    cod-h₁ : Space
    cod-h₁ = Subspace dom⟦u₄⟧ (λ w → pr₁ (pr₁ ⟦u₄⟧ w) ≡ (f , pr₁ fan f))
          -- ⟪ dom⟦u₄⟧ , Γ² ⟫ ⟪ dom⟦u₄⟧ , Γ³ , Γ² ⟫ ⟦u₅'⟧ ○ ⟦u₄⟧ ⁻¹₍ (f , pr₁ 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 → pr₁ w ≡ ((f₁ , n₁) , α))
            -- ⟪ Γ⁴ , Γ³ ⟫ ⟦u₄'⟧ ⁻¹₍ ((f₁ , n₁) , α) ₎
      cod-h₂ : Space
      cod-h₂ = Subspace dom⟦u₃⟧ (λ w → pr₁ (pr₁ ⟦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 → pr₁ w ≡ (((f₂ , n₂) , α₂) , β))
              -- ⟪ dom⟦u₁⟧ , Γ⁴ ⟫ ⟦u₁⟧ ⁻¹₍ (((f₂ , n₂) , α₂) , β) ₎
        cod-h₃ : Space
        cod-h₃ = Subspace dom⟦u₂⟧ (λ w → pr₁ (pr₁ 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 , pr₁ fan f) ]
--        e₂ : [ ((f₂ , n₂) , α₂) ≡ ((f₁ , n₁) , α) ]
--        e₃ : [ (((f₃ , n₃) , α₃) , β₃) ≡ (((f₂ , n₂) , α₂) , β) ]
          eq₃₂ : (f₃ , n₃) ≡ (f₂ , n₂)
          eq₃₂ = ap (pr₁ ∘ pr₁) e₃
          eq₂₁ : (f₂ , n₂) ≡ (f₁ , n₁)
          eq₂₁ = ap pr₁ e₂
          eq₃₀ : (f₃ , n₃) ≡ (f , pr₁ fan f)
          eq₃₀ = eq₃₂  · eq₂₁ · e₁
          eqf : f₃ ≡ f
          eqf = ap pr₁ eq₃₀
          eqn : n₃ ≡ pr₁ fan f
          eqn = ap pr₂ eq₃₀
          eqn₃ : n₃ ≡ pr₁ fan f₃
          eqn₃ = transport (λ x → n₃ ≡ pr₁ fan x) (eqf ⁻¹) eqn
          en₃' : pr₁ α₃ ≡[ pr₁ fan f₃ ] pr₁ β₃
          en₃' = transport (λ x → pr₁ α₃ ≡[ x ] pr₁ β₃) eqn₃ en₃
          goal : pr₁ f₃ α₃ ≡ pr₁ f₃ β₃
          goal = fan-behaviour f₃ α₃ β₃ en₃'
                 -------------
        cts₃ : continuous dom-h₃ cod-h₃ h₃
            -- ∀(p : ₂ℕ → U dom-h₃) → pr₁ ∘ pr₁ ∘ p ∈ Probe Γ⁴ →
            -- pr₁ ∘ pr₁ ∘ pr₁ ∘ h₃ ∘ p ∈ Probe Γ⁴
        cts₃ _ pP = pP

      cts₂ : continuous dom-h₂ cod-h₂ h₂
          -- ∀(p : ₂ℕ → U dom-h₂) → pr₁ ∘ p ∈ Probe Γ⁴ → pr₁ ∘ h₂ ∘ p ∈ Probe dom⟦u₃⟧
      cts₂ _ pP = pP , (λ _ _ _ qQ _ → qQ)

    cts₁ : continuous dom-h₁ cod-h₁ h₁
        -- ∀(p : ₂ℕ → U dom-h₁) → pr₁ ∘ p ∈ Probe Γ³ → pr₁ ∘ h₁ ∘ p ∈ Probe dom⟦u₄⟧
    cts₁ _ pP = pP , (λ _ _ _ qQ _ → qQ , (λ _ _ _ rR _ → rR))

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

\end{code}

To validate UC is equivalent to inhabit the space dom⟦uc⟧.

\begin{code}

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

Theorem : UC-is-validated
Theorem = uc

\end{code}