Chuangjie Xu 2014 (updated in February 2015)

\begin{code}

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

module UsingSetoid.ModellingUC.UCinT where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingSetoid.Setoid
open import UsingSetoid.Space.Coverage
open import UsingSetoid.Space.Space
open import UsingSetoid.Space.CartesianClosedness
open import UsingSetoid.Space.DiscreteSpace
open import UsingSetoid.Space.YonedaLemma
open import UsingSetoid.Space.Fan

\end{code}

Syntax

\begin{code}

infixr 10 _⇨_

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

infixl 10 _₊_

data Cxt : ℕ → Set where
 ε : Cxt zero
 _₊_ : {n : ℕ} → Cxt n → Ty → Cxt (succ n)

data Fin : ℕ → Set where
 zero : {n : ℕ} → Fin (succ n)
 succ : {n : ℕ} → Fin n → Fin (succ n)

_[_] : {n : ℕ} → Cxt n → Fin n → Ty
(xs ₊ x) [ zero ]   = x
(xs ₊ x) [ succ i ] = xs [ i ]

infixl 10 _∙_

data Tm : {n : ℕ} → Cxt n → Ty → Set where
 VAR  : {n : ℕ}{Γ : Cxt n}           → (i : Fin n) → Tm Γ (Γ [ i ])
 ⊥    : {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 Γ (σ ⇨ (Ⓝ ⇨ σ ⇨ σ) ⇨ Ⓝ ⇨ σ)
 LAM  : {n : ℕ}{Γ : Cxt n}{σ τ : Ty} → Tm (Γ ₊ σ) τ → Tm Γ (σ ⇨ τ)
 _∙_  : {n : ℕ}{Γ : Cxt n}{σ τ : Ty} → Tm Γ (σ ⇨ τ) → Tm Γ σ → Tm Γ τ
 FAN  : {n : ℕ}{Γ : Cxt n}           → Tm Γ (((Ⓝ ⇨ ②) ⇨ Ⓝ) ⇨ Ⓝ)

infix  10 _==_
infixr 10 _→→_

data Fml : {n : ℕ} → Cxt n → Set where
 _==_ : {n : ℕ}{Γ : Cxt n}{σ : Ty} → Tm Γ σ → Tm Γ σ → Fml Γ
 _→→_ : {n : ℕ}{Γ : Cxt n}         → Fml Γ  → Fml Γ  → Fml Γ

\end{code}

Interpretation

\begin{code}

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

⟦_⟧ᶜ : {n : ℕ} → Cxt n → Space
⟦ ε ⟧ᶜ = ⒈Space
⟦ Γ ₊ A ⟧ᶜ = ⟦ Γ ⟧ᶜ ⊗ ⟦ A ⟧ʸ

Eprj : {n : ℕ}(Γ : Cxt n)(i : Fin n) → E-map (U ⟦ Γ ⟧ᶜ) (U ⟦ Γ [ i ] ⟧ʸ)
Eprj {0}      ε       ()
Eprj {succ n} (Γ ₊ σ)  zero    = (prj₀ , eprj₀)
 where
  prj₀ : G ⟦ Γ ₊ σ ⟧ᶜ → G ⟦ σ ⟧ʸ
  prj₀ (_ , x) = x
  eprj₀ : ∀ xs xs' → E (U ⟦ Γ ₊ σ ⟧ᶜ) xs xs' → E (U ⟦ σ ⟧ʸ) (prj₀ xs) (prj₀ xs')
  eprj₀ _ _ (_ , e) = e
Eprj {succ n} (Γ ₊ σ) (succ i) = (prjᵢ₊₁ , eprjᵢ₊₁)
 where
  prjᵢ : G ⟦ Γ ⟧ᶜ → G ⟦ Γ [ i ] ⟧ʸ
  prjᵢ = pr₁ (Eprj Γ i)
  eprjᵢ : ∀ xs xs' → E (U ⟦ Γ ⟧ᶜ) xs xs' → E (U ⟦ Γ [ i ] ⟧ʸ) (prjᵢ xs) (prjᵢ xs')
  eprjᵢ = pr₂ (Eprj Γ i)
  prjᵢ₊₁ : G ⟦ Γ ₊ σ ⟧ᶜ → G ⟦ (Γ ₊ σ) [ succ i ] ⟧ʸ
  prjᵢ₊₁ (xs , _) = prjᵢ xs
  eprjᵢ₊₁ : ∀ xs xs' → E (U ⟦ Γ ₊ σ ⟧ᶜ) xs xs' → E (U ⟦ (Γ ₊ σ) [ succ i ] ⟧ʸ) (prjᵢ₊₁ xs) (prjᵢ₊₁ xs')
  eprjᵢ₊₁ (xs , _) (xs' , _) (ex , _) = eprjᵢ xs xs' ex

Eprj-is-continuous : {n : ℕ}(Γ : Cxt n)(i : Fin n) → continuous ⟦ Γ ⟧ᶜ ⟦ Γ [ i ] ⟧ʸ (Eprj Γ i)
Eprj-is-continuous {0}       ε      ()
Eprj-is-continuous {succ n} (Γ ₊ σ)  zero    = λ _ → pr₂
Eprj-is-continuous {succ n} (Γ ₊ σ) (succ i) = λ p pΓσ →
    Eprj-is-continuous Γ i (⟨ U ⟦ Γ ₊ σ ⟧ᶜ ∣ U ⟦ Γ ⟧ᶜ ⟩ E-pr₁ (U ⟦ Γ ⟧ᶜ) (U ⟦ σ ⟧ʸ) ◎ p) (pr₁ pΓσ)

continuous-prj : {n : ℕ}(Γ : Cxt n)(i : Fin n) → Map ⟦ Γ ⟧ᶜ ⟦ Γ [ i ] ⟧ʸ
continuous-prj Γ i = Eprj Γ i , Eprj-is-continuous Γ i


⟦_⟧ᵐ : {n : ℕ}{Γ : Cxt n}{σ : Ty} → Tm Γ σ → Map ⟦ Γ ⟧ᶜ ⟦ σ ⟧ʸ
⟦ VAR {n} {Γ} i ⟧ᵐ           = continuous-prj Γ i
⟦ ⊥ {_} {Γ} ⟧ᵐ               = continuous-constant ⟦ Γ ⟧ᶜ ⟦ ② ⟧ʸ ₀
⟦ ⊤ {_} {Γ} ⟧ᵐ               = continuous-constant ⟦ Γ ⟧ᶜ ⟦ ② ⟧ʸ ₁
⟦ IF {_} {Γ} {σ} ⟧ᵐ          = continuous-constant ⟦ Γ ⟧ᶜ ⟦ ② ⇨ σ ⇨ σ ⇨ σ ⟧ʸ (continuous-if ⟦ σ ⟧ʸ)
⟦ ZERO {_} {Γ} ⟧ᵐ            = continuous-constant ⟦ Γ ⟧ᶜ ⟦ Ⓝ ⟧ʸ 0
⟦ SUCC {_} {Γ} ⟧ᵐ            = continuous-constant ⟦ Γ ⟧ᶜ ⟦ Ⓝ ⇨ Ⓝ ⟧ʸ continuous-succ
⟦ REC {_} {Γ} {σ} ⟧ᵐ         = continuous-constant ⟦ Γ ⟧ᶜ ⟦ σ ⇨ (Ⓝ ⇨ σ ⇨ σ) ⇨ Ⓝ ⇨ σ ⟧ʸ (continuous-rec ⟦ σ ⟧ʸ)
⟦ LAM {n} {Γ} {σ} {τ} M ⟧ᵐ   = continuous-λ ⟦ Γ ⟧ᶜ ⟦ σ ⟧ʸ ⟦ τ ⟧ʸ ⟦ M ⟧ᵐ
⟦ _∙_ {n} {Γ} {σ} {τ} M N ⟧ᵐ = continuous-app ⟦ Γ ⟧ᶜ ⟦ σ ⟧ʸ ⟦ τ ⟧ʸ ⟦ M ⟧ᵐ ⟦ N ⟧ᵐ
⟦ FAN {_} {Γ} ⟧ᵐ             = continuous-constant ⟦ Γ ⟧ᶜ ⟦ ((Ⓝ ⇨ ②) ⇨ Ⓝ) ⇨ Ⓝ ⟧ʸ fan


⟦_⟧ᶠ : {n : ℕ}{Γ : Cxt n} → Fml Γ → G ⟦ Γ ⟧ᶜ → Set
⟦ t == u ⟧ᶠ ρ = pr₁ (pr₁ ⟦ t ⟧ᵐ) ρ ≡ pr₁ (pr₁ ⟦ u ⟧ᵐ) ρ
⟦ φ →→ ψ ⟧ᶠ ρ = (⟦ φ ⟧ᶠ ρ) → (⟦ ψ ⟧ᶠ ρ)

\end{code}

We say a formula is validated by the model if

\begin{code}

_is-validated : {n : ℕ}{Γ : Cxt n} → Fml Γ → Set
φ is-validated = ∀ ρ → ⟦ φ ⟧ᶠ ρ

\end{code}

Formulation of the uniform-continuity principle within T:

\begin{code}

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

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

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

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 = refl , refl


ν₀ : {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)))

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

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

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

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

A≡[FAN•F]B : Tm Γ ②
A≡[FAN•F]B = REC ∙ ⊤ ∙ (LAM (LAM (MIN (EQ (A' ∙ ν₁) (B' ∙ ν₁)) ν₀))) ∙ (FAN ∙ F)

Principle[UC] : Fml Γ
Principle[UC] = (A≡[FAN•F]B == ⊤) →→ (F ∙ A == F ∙ B)

\end{code}

The uniform-continuity principle is validated by the model:

\begin{code}

Theorem : Principle[UC] is-validated
       -- ∀(ρ : U ⟦ Γ ⟧ᶜ) → ⟦ (A≡[FAN•F]B == ⊤) →→ (F ∙ A == F ∙ B) ⟧ᶠ ρ
Theorem ρ EN = fan-behaviour f α β en
 where
  f : Map (ℕSpace ⇒ ₂Space) ℕSpace
  f = pr₁ (pr₁ ⟦ F ⟧ᵐ) ρ
  α β : Map ℕSpace ₂Space
  α = pr₁ (pr₁ ⟦ A ⟧ᵐ) ρ
  β = pr₁ (pr₁ ⟦ B ⟧ᵐ) ρ

  g : ℕ → ₂ → ₂
  g n b = pr₁ (pr₁ (pr₁ (pr₁ (pr₁ (pr₁ ⟦ LAM (LAM (MIN (EQ (A' ∙ ν₁) (B' ∙ ν₁)) ν₀)) ⟧ᵐ) ρ)) n)) b

  lemma : (k : ℕ) → rec ₁ g k ≡ ₁ → pr₁ (pr₁ α) ≡[ k ] pr₁ (pr₁ β)
  lemma 0        refl = ≡[zero]
  lemma (succ k) esk  = ≡[succ] IH claim₁
   where
    ek : rec ₁ g k ≡ ₁
    ek = pr₂ (Lemma[min] (eq (pr₁ (pr₁ α) k) (pr₁ (pr₁ β) k)) (rec ₁ g k) esk)
    IH : pr₁ (pr₁ α) ≡[ k ] pr₁ (pr₁ β)
    IH = lemma k ek
    claim₀ : eq (pr₁ (pr₁ α) k) (pr₁ (pr₁ β) k) ≡ ₁
    claim₀ = pr₁ (Lemma[min] (eq (pr₁ (pr₁ α) k) (pr₁ (pr₁ β) k)) (rec ₁ g k) esk)
    claim₁ : pr₁ (pr₁ α) k ≡ pr₁ (pr₁ β) k
    claim₁ = Lemma[eq] (pr₁ (pr₁ α) k) (pr₁ (pr₁ β) k) claim₀

  -- By the above lemma and the assumption that ⟦ A≡[FAN•F]B == ⊤ ⟧ᶠ ρ ≡ ₁,
  -- the interpretations of the two sequences are equal up to the first ⟦ N ⟧ᵐ position.
  en : pr₁ (pr₁ (pr₁ (pr₁ ⟦ A ⟧ᵐ) ρ)) ≡[ pr₁ (pr₁ ⟦ FAN ∙ F ⟧ᵐ) ρ ] pr₁ (pr₁ (pr₁ (pr₁ ⟦ B ⟧ᵐ) ρ))
  en = lemma (pr₁ (pr₁ ⟦ FAN ∙ F ⟧ᵐ) ρ) EN

\end{code}