Chuangjie Xu, 2013

\begin{code}

module HAomega where

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

\end{code}

Vectors, to represent contexts:

\begin{code}

infixl  _₊_

data _^_ (X : Set) : ℕ → Set where
 ε : X ^ 
 _₊_ : {n : ℕ} → X ^ n → X → X ^ (succ n)

\end{code}

Index function of vectors

\begin{code}

_₍_₎ : {X : Set} {n : ℕ} → X ^ n → Fin n → X
(xs ₊ x) ₍ zero ₎   = x
(xs ₊ x) ₍ succ i ₎ = xs ₍ i ₎

\end{code}

Types of system T:

\begin{code}

infixl  _⊠_
infixr  _⇨_

data Ty : Set where
 ⓪ : Ty
 ① : Ty
 ② : Ty
 Ⓝ : Ty
 _⊠_ : Ty → Ty → Ty
 _⊞_ : Ty → Ty → Ty
 _⇨_ : Ty → Ty → Ty

\end{code}

Contexts of system T

\begin{code}

Cxt : ℕ → Set
Cxt n = Ty ^ n

\end{code}

Terms in context of system T

\begin{code}

infixl  _∙_
infixl  _ˣ_

data Tm : {n : ℕ} → Cxt n → Ty → Set where
 EMPTY : {n : ℕ}{Γ : Cxt n}{σ : Ty}     → Tm Γ (⓪ ⇨ σ)
 ●     : {n : ℕ}{Γ : Cxt n}             → Tm Γ ①
 UNIT  : {n : ℕ}{Γ : Cxt n}{σ : Ty}     → Tm Γ (σ ⇨ ①)
 ⊥     : {n : ℕ}{Γ : Cxt n}             → Tm Γ ②
 ⊤     : {n : ℕ}{Γ : Cxt n}             → Tm Γ ②
 IF    : {n : ℕ}{Γ : Cxt n}{σ : Ty}     → Tm Γ (σ ⇨ σ ⇨ ② ⇨ σ)
 ZERO  : {n : ℕ}{Γ : Cxt n}             → Tm Γ Ⓝ
 SUCC  : {n : ℕ}{Γ : Cxt n}             → Tm Γ (Ⓝ ⇨ Ⓝ)
 REC   : {n : ℕ}{Γ : Cxt n}{σ : Ty}     → Tm Γ (σ ⇨ (Ⓝ ⇨ σ ⇨ σ) ⇨ Ⓝ ⇨ σ)
 VAR   : {n : ℕ}{Γ : Cxt n}             → (i : Fin n) → Tm Γ (Γ ₍ i ₎)
 _ˣ_   : {n : ℕ}{Γ : Cxt n}{σ τ : Ty}   → Tm Γ σ → Tm Γ τ → Tm Γ (σ ⊠ τ)
 PRJ₀  : {n : ℕ}{Γ : Cxt n}{σ τ : Ty}   → Tm Γ ((σ ⊠ τ) ⇨ σ)
 PRJ₁  : {n : ℕ}{Γ : Cxt n}{σ τ : Ty}   → Tm Γ ((σ ⊠ τ) ⇨ τ)
 IN₀   : {n : ℕ}{Γ : Cxt n}{σ τ : Ty}   → Tm Γ (σ ⇨ (σ ⊞ τ))
 IN₁   : {n : ℕ}{Γ : Cxt n}{σ τ : Ty}   → Tm Γ (τ ⇨ (σ ⊞ τ))
 CASE  : {n : ℕ}{Γ : Cxt n}{σ τ δ : Ty} → Tm Γ ((σ ⇨ δ) ⇨ (τ ⇨ δ) ⇨ (σ ⊞ τ) ⇨ δ)
 LAM   : {n : ℕ}{Γ : Cxt n}{σ τ : Ty}   → Tm (Γ ₊ σ) τ → Tm Γ (σ ⇨ τ)
 _∙_   : {n : ℕ}{Γ : Cxt n}{σ τ : Ty}   → Tm Γ (σ ⇨ τ) → Tm Γ σ → Tm Γ τ

\end{code}

Interpretation of types in C-spaces:

\begin{code}

【_】 : Ty → Space
【 ⓪ 】 = ∅Space
【 ① 】 = ⒈Space
【 ② 】 = ₂Space
【 Ⓝ 】 = ℕSpace
【 σ ⊠ τ 】 = 【 σ 】 ⊗ 【 τ 】
【 σ ⊞ τ 】 = 【 σ 】 ⊕ 【 τ 】
【 σ ⇨ τ 】 = 【 σ 】 ⇒ 【 τ 】

\end{code}

Interpretation of contexts in C-spaces:

\begin{code}

〖_〗 : {n : ℕ} → Cxt n → Space
〖 ε 〗      = ⒈Space
〖 σs ₊ σ 〗 = 〖 σs 〗 ⊗ 【 σ 】

\end{code}

Interpretation of the index function in C-spaces, which is continuous:

\begin{code}

_﹝_﹞ : {n : ℕ}{Γ : Cxt n} → U 〖 Γ 〗 → (i : Fin n) → U 【 Γ ₍ i ₎ 】
_﹝_﹞ {}      {ε}      ⋆        ()
_﹝_﹞ {succ n} {σs ₊ σ} (xs , x) zero     = x
_﹝_﹞ {succ n} {σs ₊ σ} (xs , x) (succ i) = xs ﹝ i ﹞

﹝﹞-is-continuous : {n : ℕ}{Γ : Cxt n}{i : Fin n} → continuous {〖 Γ 〗} {【 Γ ₍ i ₎ 】} (λ xs → xs ﹝ i ﹞)
﹝﹞-is-continuous {}      {ε}     {()}
﹝﹞-is-continuous {succ n} {Γ ₊ σ} {zero}   = λ _ → ∧-elim₁
﹝﹞-is-continuous {succ n} {Γ ₊ σ} {succ i} = λ p pΓσ → IH (π₀ ∘ p) (∧-elim₀ pΓσ)
 where
  IH : continuous {〖 Γ 〗} {【 Γ ₍ i ₎ 】} (λ xs → xs ﹝ i ﹞)
  IH = ﹝﹞-is-continuous {n} {Γ} {i}

\end{code}

Interpretations of terms in context, which are continuous functions from the
interpretations of contexts to the ones of types:

\begin{code}

⟦_⟧ : {n : ℕ}{Γ : Cxt n}{σ : Ty} → Tm Γ σ → Map 〖 Γ 〗 【 σ 】
⟦ EMPTY {n} {Γ} {σ} ⟧        = (λ _ → continuous-empty {【 σ 】}) ,
                              (λ _ _ p p⓪ _ _ → π₁ (continuous-empty {【 σ 】}) p p⓪)
⟦ ● ⟧                        = (λ _ → ⋆) , (λ _ _ → ⋆)
⟦ UNIT {n} {Γ} {σ} ⟧         = (λ _ → continuous-unit {【 σ 】}) ,
                              (λ _ _ p pσ _ _ → π₁ (continuous-unit {【 σ 】}) p pσ)
⟦ ⊥ ⟧                        = (λ _ → ₀) , (λ _ _ →  , (λ _ _ _ → refl) , (λ _ _ → ≤-zero))
⟦ ⊤ ⟧                        = (λ _ → ₁) , (λ _ _ →  , (λ _ _ _ → refl) , (λ _ _ → ≤-zero))
⟦ IF {n} {Γ} {σ} ⟧           = (λ _ → continuous-if {【 σ 】}) ,
                              (λ _ _ p pσ _ _ → π₁ (continuous-if {【 σ 】}) p pσ)
⟦ ZERO ⟧                     = (λ _ → ) , (λ _ _ →  , (λ _ _ _ → refl) , (λ _ _ → ≤-zero))
⟦ SUCC ⟧                     = (λ _ → continuous-succ) , (λ _ _ p pN _ _ → π₁ continuous-succ p pN)
⟦ REC {n} {Γ} {σ} ⟧          = (λ _ → continuous-rec {【 σ 】}) ,
                              (λ _ _ p pσ _ _ → π₁ (continuous-rec {【 σ 】}) p pσ)
⟦ VAR {n} {Γ} i ⟧            = (λ ρ → ρ ﹝ i ﹞) , ﹝﹞-is-continuous {n} {Γ} {i}
⟦ M ˣ N ⟧                    = (λ ρ → π₀ ⟦ M ⟧ ρ , π₀ ⟦ N ⟧ ρ) ,
                              (λ p pΓ → π₁ ⟦ M ⟧ p pΓ , π₁ ⟦ N ⟧ p pΓ)
⟦ PRJ₀ {n} {Γ} {σ} {τ} ⟧     = (λ _ → continuous-π₀ {【 σ 】} {【 τ 】}) ,
                              (λ _ _ p pστ _ _ → π₁ (continuous-π₀ {【 σ 】} {【 τ 】}) p pστ)
⟦ PRJ₁ {n} {Γ} {σ} {τ} ⟧     = (λ _ → continuous-π₁ {【 σ 】} {【 τ 】}) ,
                              (λ _ _ p pστ _ _ → π₁ (continuous-π₁ {【 σ 】} {【 τ 】}) p pστ)
⟦ IN₀ {n} {Γ} {σ} {τ} ⟧      = (λ _ → continuous-in₀ {【 σ 】} {【 τ 】}) ,
                              (λ _ _ p pσ _ _ → π₁ (continuous-in₀ {【 σ 】} {【 τ 】}) p pσ)
⟦ IN₁ {n} {Γ} {σ} {τ} ⟧      = (λ _ → continuous-in₁ {【 σ 】} {【 τ 】}) ,
                              (λ _ _ p pτ _ _ → π₁ (continuous-in₁ {【 σ 】} {【 τ 】}) p pτ)
⟦ CASE {n} {Γ} {σ} {τ} {δ} ⟧ = (λ _ → continuous-case {【 σ 】} {【 τ 】} {【 δ 】}) ,
                              (λ _ _ p pσδ _ _ → π₁ (continuous-case {【 σ 】} {【 τ 】} {【 δ 】}) p pσδ)
⟦ LAM {n} {Γ} {σ} {τ} M ⟧    = f , cts-f
 where
  f : U 〖 Γ 〗 → U 【 σ ⇨ τ 】
  f xs = g , cts-g
   where
    g : U 【 σ 】 → U 【 τ 】
    g x = π₀ ⟦ M ⟧ (xs , x)
    cts-g : continuous {【 σ 】} {【 τ 】} g
    cts-g p pσ = π₁ ⟦ M ⟧ q qΓσ
     where
      q : ₂ℕ → U 〖 Γ ₊ σ 〗
      q α = (xs , p α)
      qΓσ : q ∈ Probe 〖 Γ ₊ σ 〗
      qΓσ = cond₀ 〖 Γ 〗 (λ _ → xs) (λ _ _ → refl) , pσ
  cts-f : continuous {〖 Γ 〗} {【 σ ⇨ τ 】} f
  cts-f p pΓ q qσ t uc = π₁ ⟦ M ⟧ r rΓσ
   where
    r : ₂ℕ → U 〖 Γ ₊ σ 〗
    r α = (p(t α) , q α)
    rΓσ : r ∈ Probe 〖 Γ ₊ σ 〗
    rΓσ = cond₁ 〖 Γ 〗 t uc p pΓ , qσ
⟦ _∙_ {n} {Γ} {σ} {τ} M N ⟧ = f , cts-f
 where
  f : U 〖 Γ 〗 → U 【 τ 】
  f xs = π₀ (π₀ ⟦ M ⟧ xs) (π₀ ⟦ N ⟧ xs)
  cts-f : continuous {〖 Γ 〗} {【 τ 】} f
  cts-f p pΓ = π₁ ⟦ M ⟧ p pΓ ((π₀ ⟦ N ⟧) ∘ p) (π₁ ⟦ N ⟧ p pΓ) id Lemma[id-UC]

\end{code}

HAω formulas:

\begin{code}

infix   _⌸_
infixl  _⍓_
infixr  _⍈_
infixr  Ā_‣_
infixr  Ē_‣_

data HAω : {n : ℕ} → Cxt n → Set where
 _⌸_  : {n : ℕ}{Γ : Cxt n}{σ : Ty} → Tm Γ σ → Tm Γ σ → HAω Γ
 _⍓_  : {n : ℕ}{Γ : Cxt n} → HAω Γ → HAω Γ → HAω Γ
 _⍌_  : {n : ℕ}{Γ : Cxt n} → HAω Γ → HAω Γ → HAω Γ
 _⍈_  : {n : ℕ}{Γ : Cxt n} → HAω Γ → HAω Γ → HAω Γ
 Ā_‣_ : {n : ℕ}{Γ : Cxt n} → (σ : Ty) → HAω (Γ ₊ σ) → HAω Γ
 Ē_‣_ : {n : ℕ}{Γ : Cxt n} → (σ : Ty) → HAω (Γ ₊ σ) → HAω Γ

\end{code}

Translations of formulas to T types:

\begin{code}

∣_∣ : {n : ℕ}{Γ : Cxt n} → HAω Γ → Ty
∣ M ⌸ N ∣   = ①
∣ φ ⍓ ψ ∣   = ∣ φ ∣ ⊠ ∣ ψ ∣
∣ φ ⍌ ψ ∣   = ∣ φ ∣ ⊞ ∣ ψ ∣
∣ φ ⍈ ψ ∣   = ∣ φ ∣ ⇨ ∣ ψ ∣
∣ Ā σ ‣ φ ∣ = σ ⇨ ∣ φ ∣
∣ Ē σ ‣ φ ∣ = σ ⊠ ∣ φ ∣

\end{code}

Realizability relation:

\begin{code}

infix  _is-realized-by_

_is-realized-by_ : {n : ℕ}{Γ : Cxt n} → (φ : HAω Γ) → U 〖 Γ 〗 × U 【 ∣ φ ∣ 】 → Set
(M ⌸ N)   is-realized-by (ρ , ⋆)     = π₀ ⟦ M ⟧ ρ ≡ π₀ ⟦ N ⟧ ρ
(φ ⍓ ψ)   is-realized-by (ρ , x , y) = φ is-realized-by (ρ , x) ∧ ψ is-realized-by (ρ , y)
(φ ⍌ ψ)   is-realized-by (ρ , in₀ x) = φ is-realized-by (ρ , x)
(φ ⍌ ψ)   is-realized-by (ρ , in₁ y) = ψ is-realized-by (ρ , y)
(φ ⍈ ψ)   is-realized-by (ρ , f)     = ∀(x : U 【 ∣ φ ∣ 】) → φ is-realized-by (ρ , x) → ψ is-realized-by (ρ , π₀ f x)
(Ā σ ‣ φ) is-realized-by (ρ , f)     = ∀(x : U 【 σ 】) → φ is-realized-by ((ρ , x) , π₀ f x)
(Ē σ ‣ φ) is-realized-by (ρ , x , y) = φ is-realized-by ((ρ , x) , y)

_is-realizable : {n : ℕ}{Γ : Cxt n} → HAω Γ → Set
_is-realizable {n} {Γ} φ = ∃ \(w : U 〖 Γ 〗 × U 【 ∣ φ ∣ 】) → φ is-realized-by w

\end{code}

Auxiliaries to express UC in HAω:

EQ returns ⊤ iff the two input booleans are equal. And eq is the set
interpretation of EQ.

\begin{code}

EQ : {n : ℕ}{Γ : Cxt n} → Tm Γ ② → Tm Γ ② → Tm Γ ②
EQ B₀ B₁ = IF ∙ (IF ∙ ⊤ ∙ ⊥ ∙ B₁) ∙ B₁ ∙ B₀

eq : ₂ → ₂ → ₂
eq b₀ b₁ = if (if ₁ ₀ b₁) b₁ b₀

Lemma[eq] : (b₀ b₁ : ₂) → eq b₀ b₁ ≡ ₁ → b₀ ≡ b₁
Lemma[eq] ₀ ₀ refl = refl
Lemma[eq] ₀ ₁ ()
Lemma[eq] ₁ ₀ ()
Lemma[eq] ₁ ₁ refl = refl

\end{code}

MIN returns the minimal one of the two input booleans. And min is the set
interpretation of MIN.

\begin{code}

MIN : {n : ℕ}{Γ : Cxt n} → Tm Γ ② → Tm Γ ② → Tm Γ ②
MIN B₀ B₁ = IF ∙ ⊥ ∙ B₁ ∙ B₀

min : ₂ → ₂ → ₂
min b₀ b₁ = if ₀ b₁ b₀

Lemma[min] : (b₀ b₁ : ₂) → min b₀ b₁ ≡ ₁ → b₀ ≡ ₁ ∧ b₁ ≡ ₁
Lemma[min] ₀ ₀ ()
Lemma[min] ₀ ₁ ()
Lemma[min] ₁ ₀ ()
Lemma[min] ₁ ₁ refl = ∧-intro refl refl

\end{code}

To realize UC, we work with the context

  Γ  ≡  F : (Ⓝ ⇨ ②) ⇨ Ⓝ , n : Ⓝ , A : Ⓝ ⇨ ② , B : Ⓝ ⇨ ②

Here are the projection functions for the context Γ.

\begin{code}

ν₀ : {n : ℕ}{Γ : Cxt (succ n)} →
     Tm Γ (Γ ₍ zero ₎)
ν₀ = VAR zero
ν₁ : {n : ℕ}{Γ : Cxt (succ (succ n))} →
     Tm Γ (Γ ₍ succ zero ₎)
ν₁ = VAR (succ zero)
ν₂ : {n : ℕ}{Γ : Cxt (succ (succ (succ n)))} →
     Tm Γ (Γ ₍ succ (succ zero) ₎)
ν₂ = VAR (succ (succ zero))
ν₃ : {n : ℕ}{Γ : Cxt (succ (succ (succ (succ n))))} →
     Tm Γ (Γ ₍ succ (succ (succ zero)) ₎)
ν₃ = VAR (succ (succ (succ zero)))
ν₄ : {n : ℕ}{Γ : Cxt (succ (succ (succ (succ (succ n)))))} →
     Tm Γ (Γ ₍ succ (succ (succ (succ zero))) ₎)
ν₄ = VAR (succ (succ (succ (succ zero))))
ν₅ : {n : ℕ}{Γ : Cxt (succ (succ (succ (succ (succ (succ n))))))} →
     Tm Γ (Γ ₍ succ (succ (succ (succ (succ zero)))) ₎)
ν₅ = VAR (succ (succ (succ (succ (succ zero)))))

Γ : Cxt 
Γ = ε ₊ ((Ⓝ ⇨ ②) ⇨ Ⓝ) ₊ Ⓝ ₊ (Ⓝ ⇨ ②) ₊ (Ⓝ ⇨ ②)

F : Tm Γ ((Ⓝ ⇨ ②) ⇨ Ⓝ)
F = ν₃

N : Tm Γ Ⓝ
N = ν₂

A B : Tm Γ (Ⓝ ⇨ ②)
A = ν₁
B = ν₀

\end{code}

A' and B' are the weakening of sequences A and B in context Γ.

\begin{code}

A' B' : Tm (Γ ₊ Ⓝ ₊ ②) (Ⓝ ⇨ ②)
A' = ν₃
B' = ν₂

\end{code}

The "agree with" function for the two sequences A and B.
If they are equal up to the first N positions, then A≣[N]B is ⊤.

\begin{code}

A≣[N]B : Tm Γ ②
A≣[N]B = REC ∙ ⊤ ∙ (LAM (LAM (MIN (EQ (A' ∙ ν₁) (B' ∙ ν₁)) ν₀))) ∙ N

\end{code}

The axiom of uniform continuity and its realizer:

\begin{code}

Axiom[Uniform-Continuity] : HAω ε
Axiom[Uniform-Continuity] =
   Ā (Ⓝ ⇨ ②) ⇨ Ⓝ     ‣ Ē Ⓝ     ‣ Ā Ⓝ ⇨ ②     ‣ Ā Ⓝ ⇨ ②     ‣  A≣[N]B ⌸ ⊤  ⍈  F ∙ A ⌸ F ∙ B
-- ∀ f : (Ⓝ ⇨ ②) ⇨ Ⓝ . ∃ n : Ⓝ . ∀ α : Ⓝ ⇨ ② . ∀ β : Ⓝ ⇨ ② .   α ≣[n] β   →    f α ≡ f β


Theorem : Axiom[Uniform-Continuity] is-realizable
Theorem = ∃-intro (⋆ , e) prf
 where
  e : U (((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ⇒ (ℕSpace ⊗ ((ℕSpace ⇒ ₂Space) ⇒ (ℕSpace ⇒ ₂Space) ⇒ ⒈Space ⇒ ⒈Space)))
  e = g , cts-g
   where
    g : Map (ℕSpace ⇒ ₂Space) ℕSpace → ℕ × Map (ℕSpace ⇒ ₂Space) ((ℕSpace ⇒ ₂Space) ⇒ ⒈Space ⇒ ⒈Space)
    g f = π₀ fan f , g₀ , cts-g₀
     where
      g₀ : Map ℕSpace ₂Space → Map (ℕSpace ⇒ ₂Space) (⒈Space ⇒ ⒈Space)
      g₀ α = g₁ , cts-g₁
       where
        g₁ : Map ℕSpace ₂Space → Map ⒈Space ⒈Space
        g₁ β = (λ _ → ⋆) , (λ _ _ → ⋆)
        cts-g₁ : continuous {ℕSpace ⇒ ₂Space} {⒈Space ⇒ ⒈Space} g₁
        cts-g₁ _ _ _ _ _ _ = ⋆
      cts-g₀ : continuous {ℕSpace ⇒ ₂Space} {(ℕSpace ⇒ ₂Space) ⇒ ⒈Space ⇒ ⒈Space} g₀
      cts-g₀ _ _ _ _ _ _ _ _ _ _ = ⋆
    cts-g : continuous {(ℕSpace ⇒ ₂Space) ⇒ ℕSpace}
                       {ℕSpace ⊗ ((ℕSpace ⇒ ₂Space) ⇒ (ℕSpace ⇒ ₂Space) ⇒ ⒈Space ⇒ ⒈Space)} g
    cts-g p pP = π₁ fan p pP , (λ _ _ _ _ _ _ _ _ _ _ _ _ → ⋆)
  prf : Axiom[Uniform-Continuity] is-realized-by (⋆ , e)
  prf f = prf'
   where
    n : ℕ
    n = π₀ (π₀ e f)
    prf' : ∀(α β : Map ℕSpace ₂Space) →
           ∀(x : ⒈) → (A≣[N]B ⌸ ⊤) is-realized-by (((((⋆ , f) , n) , α) , β) , x) →
           π₀ f α ≡ π₀ f β
   -- i.e. π₀ ⟦ F ∙ A ⟧ ((((⋆ , f) , n) , α) , β) ≡ π₀ ⟦ F ∙ B ⟧ ((((⋆ , f) , n) , α) , β)
    prf' α β ⋆ EN = fan-behaviour f α β en
     where
      ρ : U 〖 Γ 〗
      ρ = ((((⋆ , f) , n) , α) , β)
      g : ℕ → ₂ → ₂
      g n b = π₀ (π₀ (π₀ ⟦ LAM (LAM (MIN (EQ (A' ∙ ν₁) (B' ∙ ν₁)) ν₀)) ⟧ ρ) n) b
      lemma : (k : ℕ) → rec ₁ g k ≡ ₁ → π₀ α ≣[ k ] π₀ β
      lemma         refl = ≣[zero]
      lemma (succ k) esk  = ≣[succ] IH claim₁
       where
        ek : rec ₁ g k ≡ ₁
        ek = ∧-elim₁ (Lemma[min] (eq (π₀ α k) (π₀ β k)) (rec ₁ g k)  esk)
        IH : π₀ α ≣[ k ] π₀ β
        IH = lemma k ek
        claim₀ : eq (π₀ α k) (π₀ β k) ≡ ₁
        claim₀ = ∧-elim₀ (Lemma[min] (eq (π₀ α k) (π₀ β k)) (rec ₁ g k) esk)
        claim₁ : π₀ α k ≡ π₀ β k
        claim₁ = Lemma[eq] (π₀ α k) (π₀ β k) claim₀
      en : π₀ α ≣[ n ] π₀ β
      en = lemma n EN

\end{code}