T.agda

module T where

Ḳ : {X Y : Set} → X → Y → X
Ḳ x y = x

Ṣ : {X Y Z : Set} → (X → Y → Z) → (X → Y) → X → Z
Ṣ f g x = f x (g x)

_∘_ : {X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z)
g ∘ f = λ x → g (f x)

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

rec : {X : Set} → (X → X) → X → ℕ → X
rec f x zero = x
rec f x (succ n) = f (rec f x n)

data ℕ₂ : Set where
  ₀ ₁ : ℕ₂

infixl 0 _∷_
data List (X : Set) : Set where
  [] : List X
  _∷_ : X → List X → List X

data Tree (X : Set) : Set where
  empty : Tree X
  branch : X → (ℕ₂ → Tree X) → Tree X

data Σ {X : Set} (Y : X → Set) : Set where
  _,_ : (x : X) (y : Y x) → Σ {X} Y

π₀ : {X : Set} {Y : X → Set} → (Σ λ(x : X) → Y x) → X
π₀ (x , y) = x

π₁ : {X : Set} {Y : X → Set} → (t : Σ λ(x : X) → Y x) → Y (π₀ t)
π₁ (x , y) = y

data _≡_ {X : Set} : X → X → Set where
  refl : ∀ {x : X} → x ≡ x

sym : {X : Set} → {x y : X} → x ≡ y → y ≡ x
sym refl = refl

trans : {X : Set} → {x y z : X} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : {X Y : Set} → (f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
cong f refl = refl

cong₂ : {X Y Z : Set} → (f : X → Y → Z) → {x₀ x₁ : X} {y₀ y₁ : Y} → x₀ ≡ x₁ → y₀ ≡ y₁ → f x₀ y₀ ≡ f x₁ y₁
cong₂ f refl refl = refl

data D (X Y Z : Set) : Set where
  η : Z → D X Y Z
  β : (Y → D X Y Z) → X → D X Y Z

dialogue : {X Y Z : Set} → D X Y Z → (X → Y) → Z
dialogue (η z) α = z
dialogue (β Φ x) α = dialogue (Φ (α x)) α

eloquent : {X Y Z : Set} → ((X → Y) → Z) → Set
eloquent f = Σ λ d → ∀ α → dialogue d α ≡ f α

Baire : Set
Baire = ℕ → ℕ

B : Set → Set
B = D ℕ ℕ

data _≡[_]_ {X : Set} : (ℕ → X) → List ℕ → (ℕ → X) → Set where
  [] : {α α' : ℕ → X} → α ≡[ [] ] α'
  _∷_ : {α α' : ℕ → X} {i : ℕ} {s : List ℕ} → α i ≡ α' i → α ≡[ s ] α' → α ≡[ i ∷ s ] α'

continuous : (Baire → ℕ) → Set
continuous f = (α : Baire) → Σ λ (s : List ℕ) → (α' : Baire) → α ≡[ s ] α' → f α ≡ f α'

dialogue-continuity : (d : B ℕ) → continuous (dialogue d)
dialogue-continuity (η n) α   = [] , (λ α' r → refl)
dialogue-continuity (β Φ i) α = (i ∷ s) , (λ {α' (r ∷ rs) → trans (claim₀ α' rs) (claim₁ α' r)})
  where
    IH : (i : ℕ) → continuous (dialogue (Φ (α i)))
    IH i = (dialogue-continuity (Φ (α i)))
    s : List ℕ
    s = π₀ (IH i α)
    claim₀ : (α' : Baire) → α ≡[ s ] α' → dialogue (Φ (α i)) α ≡ dialogue (Φ (α i)) α'
    claim₀ = π₁ (IH i α)
    claim₁ : (α' : Baire) → α i ≡ α' i → dialogue (Φ (α i)) α' ≡ dialogue (Φ (α' i)) α'
    claim₁ α' r = cong (λ n → dialogue (Φ n) α') r

continuity-extensional : (f g : Baire → ℕ) → (∀ α → f α ≡ g α) → continuous f → continuous g
continuity-extensional f g t c α = π₀ (c α) , (λ α' r → trans (sym (t α)) (trans (π₁ (c α) α' r) (t α')))

eloquent-is-continuous : (f : Baire → ℕ) → eloquent f → continuous f
eloquent-is-continuous f (d , e) = continuity-extensional (dialogue d) f e (dialogue-continuity d)

Cantor : Set
Cantor = ℕ → ℕ₂

C : Set → Set
C = D ℕ ℕ₂

data _≡[[_]]_ {X : Set} : (ℕ → X) → Tree ℕ → (ℕ → X) → Set where
  empty  : {α α' : ℕ → X} → α ≡[[ empty ]] α'
  branch : {α α' : ℕ → X} {i : ℕ} {s : ℕ₂ → Tree ℕ}
         → α i ≡ α' i → ((j : ℕ₂) → α ≡[[ s j ]] α') → α ≡[[ branch i s ]] α'

uniformly-continuous : (Cantor → ℕ) → Set
uniformly-continuous f = Σ λ (s : Tree ℕ) → (α α' : Cantor) → α ≡[[ s ]] α' → f α ≡ f α'

dialogue-UC : (d : C ℕ) → uniformly-continuous (dialogue d)
dialogue-UC (η n) = empty , (λ α α' n → refl)
dialogue-UC (β Φ i) = (branch i s) , (λ { α α' (branch r l) → trans (claim (α i) α α' (l (α i)))
                                                                    (cong (λ j → dialogue (Φ j) α') r) })
  where
    IH : (j : ℕ₂) → uniformly-continuous (dialogue (Φ j))
    IH j = dialogue-UC (Φ j)
    s : ℕ₂ → Tree ℕ
    s j = π₀ (IH j)
    claim : ∀ j α α' → α ≡[[ s j ]] α' → dialogue (Φ j) α ≡ dialogue (Φ j) α'
    claim j = π₁ (IH j)

UC-extentional : (f g : Cantor → ℕ) → ((α : Cantor) → f α ≡ g α)
               → uniformly-continuous f → uniformly-continuous g
UC-extentional f g t (u , c) = u , (λ α α' r → trans (sym (t α)) (trans (c α α' r) (t α')))

eloquent-is-UC : (f : Cantor → ℕ) → eloquent f → uniformly-continuous f
eloquent-is-UC f (d , e) = UC-extentional (dialogue d) f e (dialogue-UC d)

embed-ℕ₂-ℕ : ℕ₂ → ℕ
embed-ℕ₂-ℕ ₀ = zero
embed-ℕ₂-ℕ ₁ = succ zero

embed-C-B : Cantor → Baire
embed-C-B α = embed-ℕ₂-ℕ ∘ α

C-restriction : (Baire → ℕ) → (Cantor → ℕ)
C-restriction f = f ∘ embed-C-B

prune : B ℕ → C ℕ
prune (η n) = η n
prune (β Φ i) = β (λ j → prune (Φ (embed-ℕ₂-ℕ j))) i

prune-behaviour : (d : B ℕ) (α : Cantor) → dialogue (prune d) α ≡ C-restriction (dialogue d) α
prune-behaviour (η n) α = refl
prune-behaviour (β Φ n) α = prune-behaviour (Φ (embed-ℕ₂-ℕ (α n))) α

eloquent-restriction : (f : Baire → ℕ) → eloquent f → eloquent (C-restriction f)
eloquent-restriction f (d , c) = prune d , (λ α → trans (prune-behaviour d α) (c (embed-C-B α)))

data type : Set where
  ι : type
  _⇒_ : type → type → type

data T : (σ : type) → Set where
  Zero : T ι
  Succ : T (ι ⇒ ι)
  Rec  : ∀ {σ : type}     → T ((σ ⇒ σ) ⇒ σ ⇒ ι ⇒ σ)
  K    : ∀ {σ τ : type}   → T (σ ⇒ τ ⇒ σ)
  S    : ∀ {ρ σ τ : type} → T ((ρ ⇒ σ ⇒ τ) ⇒ (ρ ⇒ σ) ⇒ ρ ⇒ τ)
  _·_  : ∀ {σ τ : type}   → T (σ ⇒ τ) → T σ → T τ

infixr 1 _⇒_
infixl 1 _·_

Set⟦_⟧ : type → Set
Set⟦ ι ⟧ = ℕ
Set⟦ σ ⇒ τ ⟧ = Set⟦ σ ⟧ → Set⟦ τ ⟧

⟦_⟧ : {σ : type} → T σ → Set⟦ σ ⟧
⟦ Zero ⟧ = zero
⟦ Succ ⟧ = succ
⟦ Rec ⟧ = rec
⟦ K ⟧ = Ḳ
⟦ S ⟧ = Ṣ
⟦ t · u ⟧ = ⟦ t ⟧ ⟦ u ⟧

T-definable : {σ : type} → Set⟦ σ ⟧ → Set
T-definable {σ} x = Σ λ t → ⟦ t ⟧ ≡ x

data TΩ : (σ : type) → Set where
  Ω    : TΩ (ι ⇒ ι)
  Zero : TΩ ι
  Succ : TΩ (ι ⇒ ι)
  Rec  : ∀ {σ : type}     → TΩ ((σ ⇒ σ) ⇒ σ ⇒ ι ⇒ σ)
  K    : ∀ {σ τ : type}   → TΩ (σ ⇒ τ ⇒ σ)
  S    : ∀ {ρ σ τ : type} → TΩ ((ρ ⇒ σ ⇒ τ) ⇒ (ρ ⇒ σ) ⇒ ρ ⇒ τ)
  _·_  : ∀ {σ τ : type}   → TΩ (σ ⇒ τ) → TΩ σ → TΩ τ

⟦_⟧' : {σ : type} → TΩ σ → Baire → Set⟦ σ ⟧
⟦ Ω ⟧'     α = α
⟦ Zero ⟧'  α = zero
⟦ Succ ⟧'  α = succ
⟦ Rec ⟧'   α = rec
⟦ K ⟧'     α = Ḳ
⟦ S ⟧'     α = Ṣ
⟦ t · u ⟧' α = ⟦ t ⟧' α (⟦ u ⟧' α)

embed : {σ : type} → T σ → TΩ σ
embed Zero = Zero
embed Succ = Succ
embed Rec = Rec
embed K = K
embed S = S
embed (t · u) = embed t · embed u

kleisli-extension : {X Y : Set} → (X → B Y) → B X → B Y
kleisli-extension f (η x) = f x
kleisli-extension f (β Φ i) = β (λ j → kleisli-extension f (Φ j)) i

B-functor : {X Y : Set} → (X → Y) → B X → B Y
B-functor f = kleisli-extension (η ∘ f)

decode : {X : Set} → Baire → B X → X
decode α d = dialogue d α

decode-α-is-natural : {X Y : Set} (g : X → Y) (d : B X) (α : Baire)
                    → g (decode α d) ≡ decode α (B-functor g d)
decode-α-is-natural g (η x)   α = refl
decode-α-is-natural g (β Φ i) α = decode-α-is-natural g (Φ (α i)) α

decode-kleisli-extension : {X Y : Set} (f : X → B Y) (d : B X) (α : Baire)
                         → decode α (f (decode α d)) ≡ decode α (kleisli-extension f d)
decode-kleisli-extension f (η x)   α = refl
decode-kleisli-extension f (β Φ i) α = decode-kleisli-extension f (Φ (α i)) α

B-Set⟦_⟧ : type → Set
B-Set⟦ ι ⟧ = B Set⟦ ι ⟧
B-Set⟦ σ ⇒ τ ⟧ = B-Set⟦ σ ⟧ → B-Set⟦ τ ⟧

Kleisli-extension : {X : Set} {σ : type} → (X → B-Set⟦ σ ⟧) → B X → B-Set⟦ σ ⟧
Kleisli-extension {X} {ι} = kleisli-extension
Kleisli-extension {X} {σ ⇒ τ} g d s = Kleisli-extension (λ x → g x s) d

generic : B ℕ → B ℕ
generic = kleisli-extension (β η)

generic-diagram : (α : Baire) (d : B ℕ) → α (decode α d) ≡ decode α (generic d)
generic-diagram α (η n)   = refl
generic-diagram α (β Φ n) = generic-diagram α (Φ (α n))

zero' : B ℕ
zero' = η zero

succ' : B ℕ → B ℕ
succ' = B-functor succ

rec' : {σ : type} → (B-Set⟦ σ ⟧ → B-Set⟦ σ ⟧) → B-Set⟦ σ ⟧ → B ℕ → B-Set⟦ σ ⟧
rec' f x = Kleisli-extension (rec f x)

B⟦_⟧ : {σ : type} → TΩ σ → B-Set⟦ σ ⟧
B⟦ Ω ⟧ = generic
B⟦ Zero ⟧ = zero'
B⟦ Succ ⟧ = succ'
B⟦ Rec ⟧ = rec'
B⟦ K ⟧ = Ḳ
B⟦ S ⟧ = Ṣ
B⟦ t · u ⟧ = B⟦ t ⟧ B⟦ u ⟧

dialogue-tree : T ((ι ⇒ ι) ⇒ ι) → B ℕ
dialogue-tree t = B⟦ embed t · Ω ⟧

preservation : {σ : type} → (t : T σ) → (α : Baire) → ⟦ t ⟧ ≡ ⟦ embed t ⟧' α
preservation Zero α = refl
preservation Succ α = refl
preservation Rec α = refl
preservation K α = refl
preservation S α = refl
preservation (t · u) α = cong₂ (λ f x → f x) (preservation t α) (preservation u α)

R : {σ : type} → (Baire → Set⟦ σ ⟧) → B-Set⟦ σ ⟧ → Set
R {ι} n n' = (α : Baire) → n α ≡ decode α n'
R {σ ⇒ τ} f f' = (x : Baire → Set⟦ σ ⟧) (x' : B-Set⟦ σ ⟧) → R x x' → R (λ α → f α (x α)) (f' x')

R-kleisli-lemma : (σ : type) (g : ℕ → Baire → Set⟦ σ ⟧) (g' : ℕ → B-Set⟦ σ ⟧)
                → ((k : ℕ) → R (g k) (g' k))
                → (n : Baire → ℕ) (n' : B ℕ) → R n n' → R (λ α → (g (n α) α)) (Kleisli-extension g' n')
R-kleisli-lemma ι g g' rg n n' rn = λ α → trans (rg (n α) α)
                                         (trans (cong (λ k → decode α (g' k)) (rn α))
                                                (decode-kleisli-extension g' n' α))
R-kleisli-lemma (σ ⇒ τ) g g' rg n n' rn = λ y y' ry → R-kleisli-lemma τ (λ k α → g k α (y α))
                                                                        (λ k → g' k y')
                                                                        (λ k → rg k y y' ry) n n' rn

main-lemma : {σ : type} (t : TΩ σ) → R ⟦ t ⟧' B⟦ t ⟧
main-lemma Ω = λ n n' rn α → trans (cong α (rn α)) (generic-diagram α n')
main-lemma Zero = λ α → refl
main-lemma Succ = λ n n' rn α → trans (cong succ (rn α)) (decode-α-is-natural succ n' α)
main-lemma {(σ ⇒ .σ) ⇒ .σ ⇒ ι ⇒ .σ} Rec = lemma
           where
             lemma : (f : Baire → Set⟦ σ ⟧ → Set⟦ σ ⟧) (f' : B-Set⟦ σ ⟧ → B-Set⟦ σ ⟧) → R f f'
                   → (x : Baire → Set⟦ σ ⟧) (x' : B-Set⟦ σ ⟧) → R x x'
                   → (n : Baire → ℕ) (n' : B ℕ) → R n n'
                   → R (λ α → rec (f α) (x α) (n α)) (rec' f' x' n')
             lemma f f' rf x x' rx = R-kleisli-lemma σ g g' rg
               where
                 g : ℕ → Baire → Set⟦ σ ⟧
                 g k α = rec (f α) (x α) k
                 g' : ℕ → B-Set⟦ σ ⟧
                 g' k = rec f' x' k
                 rg : (k : ℕ) → R (g k) (g' k)
                 rg zero = rx
                 rg (succ k) = rf (g k) (g' k) (rg k)
main-lemma K = λ x x' rx y y' ry → rx
main-lemma S = λ f f' rf g g' rg x x' rx → rf x x' rx (λ α → g α (x α)) (g' x') (rg x x' rx)
main-lemma (t · u) = main-lemma t ⟦ u ⟧' B⟦ u ⟧ (main-lemma u)

dialogue-tree-correct : (t : T ((ι ⇒ ι) ⇒ ι)) (α : Baire) → ⟦ t ⟧ α ≡ decode α (dialogue-tree t)
dialogue-tree-correct t α = trans (cong (λ g → g α) (preservation t α)) (main-lemma (embed t · Ω) α)

eloquence-theorem : (f : Baire → ℕ) → T-definable f → eloquent f
eloquence-theorem f (t , r) = (dialogue-tree t) , (λ α → trans (sym (dialogue-tree-correct t α)) (cong (λ f → f α) r))

corollary₀ : (f : Baire → ℕ) → T-definable f → continuous f
corollary₀ f d = eloquent-is-continuous f (eloquence-theorem f d)

corollary₁ : (f : Baire → ℕ) → T-definable f → uniformly-continuous (C-restriction f)
corollary₁ f d = eloquent-is-UC (C-restriction f) (eloquent-restriction f (eloquence-theorem f d))

mod-cont : T ((ι ⇒ ι) ⇒ ι) → Baire → List ℕ
mod-cont t α = π₀ (corollary₀ ⟦ t ⟧ (t , refl) α)

mod-cont-obs : (t : T ((ι ⇒ ι) ⇒ ι)) (α : Baire) → mod-cont t α ≡ π₀ (dialogue-continuity (dialogue-tree t) α)
mod-cont-obs t α = refl

infixl 1 _++_
_++_ : {X : Set} → List X → List X → List X
[] ++ u = u
(x ∷ t) ++ u = x ∷ t ++ u

flattern : {X : Set} → Tree X → List X
flattern empty = []
flattern (branch x t) = x ∷ flattern (t ₀) ++ flattern (t ₁)

mod-unif : T ((ι ⇒ ι) ⇒ ι) → List ℕ
mod-unif t = flattern (π₀ (corollary₁ ⟦ t ⟧ (t , refl)))

I : {σ : type} → T (σ ⇒ σ)
I {σ} = (S {σ} {σ ⇒ σ} {σ}) · (K {σ} {σ ⇒ σ}) · (K {σ} {σ})

I-behaviour : {σ : type} {x : Set⟦ σ ⟧} → ⟦ I ⟧ x ≡ x
I-behaviour = refl

number : ℕ → T ι
number zero = Zero
number (succ n) = Succ · (number n)

t₀ : T ((ι ⇒ ι) ⇒ ι)
t₀ = K · (number 17)
t₀-interpretation : ⟦ t₀ ⟧ ≡ λ α → 17
t₀-interpretation = refl

example₀ example₀' : List ℕ
example₀ = mod-cont t₀ (λ i → i)
example₀' = mod-unif t₀

v : {γ : type} → T (γ ⇒ γ)
v = I

infixl 1 _∙_
_∙_ : {γ σ τ : type} → T (γ ⇒ σ ⇒ τ) → T (γ ⇒ σ) → T (γ ⇒ τ)
f ∙ x = S · f · x

Number : {γ : type} → ℕ → T (γ ⇒ ι)
Number n = K · (number n)

t₁ : T ((ι ⇒ ι) ⇒ ι)
t₁ = v {ι ⇒ ι} ∙ (Number {ι ⇒ ι} 17)
t₁-interpretation : ⟦ t₁ ⟧ ≡ λ α → α 17
t₁-interpretation = refl
example₁ : List ℕ
example₁ = mod-unif t₁

t₂ : T ((ι ⇒ ι) ⇒ ι)
t₂ = Rec ∙ t₁ ∙ t₁
t₂-interpretation : ⟦ t₂ ⟧ ≡ λ α → rec α (α 17) (α 17)
t₂-interpretation = refl
example₂ example₂' : List ℕ
example₂ = mod-unif t₂
example₂' = mod-cont t₂ (λ i → i)