\begin{code}
module dialogue-lambda where
\end{code}
\begin{code}
_∘_ : ∀{X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z)
g ∘ f = λ x → g(f x)
data ℕ₂ : Set where
₀ : ℕ₂
₁ : ℕ₂
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
rec : ∀{X : Set} → (ℕ → X → X) → X → ℕ → X
rec f x zero = x
rec f x (succ n) = f n (rec f x n)
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
subst : {X : Set}{Y : X → Set}{x x' : X} → x ≡ x' → Y x → Y x'
subst refl y = y
\end{code}
\begin{code}
data _^_ (X : Set) : ℕ → Set where
〈〉 : X ^ zero
_’_ : {n : ℕ} → X ^ n → X → X ^ (succ n)
infixl 6 _’_
data Fin : ℕ → Set where
zero : {n : ℕ} → Fin(succ n)
succ : {n : ℕ} → Fin n → Fin(succ n)
_[_] : {X : Set} {n : ℕ} → X ^ n → Fin n → X
(xs ’ x) [ zero ] = x
(xs ’ x) [ succ i ] = xs [ i ]
\end{code}
\begin{code}
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 α
\end{code}
\begin{code}
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) α = ([] , lemma)
where
lemma : ∀ α' → α ≡[ [] ] α' → n ≡ n
lemma α' r = refl
dialogue-continuity (β φ i) α = ((i ∷ s) , lemma)
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
lemma : ∀(α' : Baire) → α ≡[ i ∷ s ] α' → dialogue (φ(α i)) α ≡ dialogue(φ (α' i)) α'
lemma α' (r ∷ rs) = trans (claim₀ α' rs) (claim₁ α' r)
continuity-extensional : ∀(f g : Baire → ℕ) → (∀(α : 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)
\end{code}
\begin{code}
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 , lemma)
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)
lemma : ∀ α α' → α ≡[[ branch i s ]] α' → dialogue (φ (α i)) α ≡ dialogue (φ (α' i)) α'
lemma α α' (branch r l) = trans fact₀ fact₁
where
fact₀ : dialogue (φ (α i)) α ≡ dialogue (φ (α' i)) α
fact₀ = cong (λ j → dialogue(φ j) α) r
fact₁ : dialogue (φ (α' i)) α ≡ dialogue (φ (α' i)) α'
fact₁ = claim (α' i) α α' (l(α' i))
UC-extensional : ∀(f g : Cantor → ℕ) → (∀(α : Cantor) → f α ≡ g α)
→ uniformly-continuous f → uniformly-continuous g
UC-extensional 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-extensional (dialogue d) f e (dialogue-UC d)
\end{code}
\begin{code}
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 α)))
\end{code}
\begin{code}
data type : Set where
ι : type
_⇒_ : type → type → type
infixr 6 _⇒_
\end{code}
\begin{code}
Cxt : ℕ → Set
Cxt n = type ^ n
data T : {n : ℕ} (Γ : Cxt n) (σ : type) → Set where
Zero : {n : ℕ}{Γ : Cxt n} → T Γ ι
Succ : {n : ℕ}{Γ : Cxt n} → T Γ (ι ⇒ ι)
Rec : {n : ℕ}{Γ : Cxt n} → {σ : type} → T Γ ((ι ⇒ σ ⇒ σ) ⇒ σ ⇒ ι ⇒ σ)
ν : {n : ℕ}{Γ : Cxt n} → (i : Fin n) → T Γ (Γ [ i ])
ƛ : {n : ℕ}{Γ : Cxt n} → {σ τ : type} → T (Γ ’ σ) τ → T Γ (σ ⇒ τ)
_·_ : {n : ℕ}{Γ : Cxt n} → {σ τ : type} → T Γ (σ ⇒ τ) → T Γ σ → T Γ τ
infixl 6 _·_
\end{code}
\begin{code}
〖_〗 : type → Set
〖 ι 〗 = ℕ
〖 σ ⇒ τ 〗 = 〖 σ 〗 → 〖 τ 〗
【_】 : {n : ℕ} (Γ : Cxt n) → Set
【 Γ 】 = (i : Fin _) → 〖 Γ [ i ] 〗
⟨⟩ : 【 〈〉 】
⟨⟩ ()
_‚_ : {n : ℕ} {Γ : Cxt n} {σ : type} → 【 Γ 】 → 〖 σ 〗 → 【 Γ ’ σ 】
(xs ‚ x) zero = x
(xs ‚ x) (succ i) = xs i
infixl 6 _‚_
⟦_⟧ : {n : ℕ} {Γ : Cxt n} {σ : type} → T Γ σ → 【 Γ 】 → 〖 σ 〗
⟦ Zero ⟧ _ = zero
⟦ Succ ⟧ _ = succ
⟦ Rec ⟧ _ = rec
⟦ ν i ⟧ xs = xs i
⟦ ƛ t ⟧ xs = λ x → ⟦ t ⟧ (xs ‚ x)
⟦ t · u ⟧ xs = (⟦ t ⟧ xs) (⟦ u ⟧ xs)
\end{code}
\begin{code}
T₀ : type → Set
T₀ = T 〈〉
⟦_⟧₀ : {σ : type} → T₀ σ → 〖 σ 〗
⟦ t ⟧₀ = ⟦ t ⟧ ⟨⟩
T-definable : ∀{σ : type} → 〖 σ 〗 → Set
T-definable x = Σ \t → ⟦ t ⟧₀ ≡ x
\end{code}
\begin{code}
data T' : {n : ℕ} (Γ : Cxt n) (σ : type) → Set where
Ω : {n : ℕ}{Γ : Cxt n} → T' Γ (ι ⇒ ι)
Zero : {n : ℕ}{Γ : Cxt n} → T' Γ ι
Succ : {n : ℕ}{Γ : Cxt n} → T' Γ (ι ⇒ ι)
Rec : {n : ℕ}{Γ : Cxt n} → {σ : type} → T' Γ ((ι ⇒ σ ⇒ σ) ⇒ σ ⇒ ι ⇒ σ)
ν : {n : ℕ}{Γ : Cxt n} → (i : Fin n) → T' Γ (Γ [ i ])
ƛ : {n : ℕ}{Γ : Cxt n} → {σ τ : type} → T' (Γ ’ σ) τ → T' Γ (σ ⇒ τ)
_·_ : {n : ℕ}{Γ : Cxt n} → {σ τ : type} → T' Γ (σ ⇒ τ) → T' Γ σ → T' Γ τ
⟦_⟧' : {n : ℕ} {Γ : Cxt n} {σ : type} → T' Γ σ → Baire → 【 Γ 】 → 〖 σ 〗
⟦ Ω ⟧' α _ = α
⟦ Zero ⟧' _ _ = zero
⟦ Succ ⟧' _ _ = succ
⟦ Rec ⟧' _ _ = rec
⟦ ν i ⟧' _ xs = xs i
⟦ ƛ t ⟧' α xs = λ x → ⟦ t ⟧' α (xs ‚ x)
⟦ t · u ⟧' α xs = (⟦ t ⟧' α xs) (⟦ u ⟧' α xs)
\end{code}
\begin{code}
embed : {n : ℕ} {Γ : Cxt n} {σ : type} → T Γ σ → T' Γ σ
embed Zero = Zero
embed Succ = Succ
embed Rec = Rec
embed (ν i) = ν i
embed (ƛ t) = ƛ(embed t)
embed (t · u) = (embed t) · (embed u)
\end{code}
\begin{code}
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)) α
\end{code}
\begin{code}
B〖_〗 : type → Set
B〖 ι 〗 = B(〖 ι 〗)
B〖 σ ⇒ τ 〗 = B〖 σ 〗 → B〖 τ 〗
\end{code}
\begin{code}
Kleisli-extension : ∀{X : Set} {σ : type} → (X → B〖 σ 〗) → B X → B〖 σ 〗
Kleisli-extension {X} {ι} = kleisli-extension
Kleisli-extension {X} {σ ⇒ τ} = λ g d s → Kleisli-extension {X} {τ} (λ x → g x s) d
\end{code}
\begin{code}
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 ℕ → B〖 σ 〗 → B〖 σ 〗) → B〖 σ 〗 → B ℕ → B〖 σ 〗
rec' f x = Kleisli-extension(rec (f ∘ η) x)
\end{code}
\begin{code}
B【_】 : {n : ℕ} (Γ : Cxt n) → Set
B【 Γ 】 = (i : Fin _) → B〖 Γ [ i ] 〗
⟪⟫ : B【 〈〉 】
⟪⟫ ()
_‚‚_ : {n : ℕ} {Γ : Cxt n} {σ : type} → B【 Γ 】 → B〖 σ 〗 → B【 Γ ’ σ 】
(xs ‚‚ x) zero = x
(xs ‚‚ x) (succ i) = xs i
\end{code}
\begin{code}
B⟦_⟧ : {n : ℕ} {Γ : Cxt n} {σ : type} → T' Γ σ → B【 Γ 】 → B〖 σ 〗
B⟦ Ω ⟧ _ = generic
B⟦ Zero ⟧ _ = zero'
B⟦ Succ ⟧ _ = succ'
B⟦ Rec ⟧ _ = rec'
B⟦ ν i ⟧ xs = xs i
B⟦ ƛ t ⟧ xs = λ x → B⟦ t ⟧ (xs ‚‚ x)
B⟦ t · u ⟧ xs = (B⟦ t ⟧ xs) (B⟦ u ⟧ xs)
\end{code}
\begin{code}
dialogue-tree : T₀((ι ⇒ ι) ⇒ ι) → B ℕ
dialogue-tree t = B⟦ (embed t) · Ω ⟧ ⟪⟫
\end{code}
\begin{code}
preservation : {n : ℕ} {Γ : Cxt n} {σ : type} (t : T Γ σ) (α : Baire) → ⟦ t ⟧ ≡ ⟦ embed t ⟧' α
preservation Zero α = refl
preservation Succ α = refl
preservation Rec α = refl
preservation (ν i) α = refl
preservation (ƛ t) α = cong (λ f → λ xs x → f(xs ‚ x)) (preservation t α)
preservation (t · u) α = cong₂ (λ f g x → f x (g x)) (preservation t α) (preservation u α)
\end{code}
\begin{code}
R : ∀{σ : type} → (Baire → 〖 σ 〗) → B〖 σ 〗 → Set
R {ι} n n' = ∀(α : Baire) → n α ≡ decode α n'
R {σ ⇒ τ} f f' = ∀(x : Baire → 〖 σ 〗) (x' : B〖 σ 〗) → R {σ} x x' → R {τ} (λ α → f α (x α)) (f' x')
\end{code}
\begin{code}
R-kleisli-lemma : ∀(σ : type) (g : ℕ → Baire → 〖 σ 〗) (g' : ℕ → B〖 σ 〗)
→ (∀(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 (fact₃ α) (fact₀ α)
where
fact₀ : ∀ α → decode α (g' (decode α n')) ≡ decode α (kleisli-extension g' n')
fact₀ = decode-kleisli-extension g' n'
fact₁ : ∀ α → g (n α) α ≡ decode α (g'(n α))
fact₁ α = rg (n α) α
fact₂ : ∀ α → decode α (g' (n α)) ≡ decode α (g' (decode α n'))
fact₂ α = cong (λ k → decode α (g' k)) (rn α)
fact₃ : ∀ α → g (n α) α ≡ decode α (g' (decode α n'))
fact₃ α = trans (fact₁ α) (fact₂ α)
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
\end{code}
\begin{code}
Rs : ∀{n : ℕ} {Γ : Cxt n} → (Baire → 【 Γ 】) → B【 Γ 】 → Set
Rs {n} {Γ} xs ys = ∀(i : Fin n) → R {Γ [ i ]} (λ α → xs α i) (ys i)
main-lemma : ∀{n : ℕ} {Γ : Cxt n} {σ : type} (t : T' Γ σ) (xs : Baire → 【 Γ 】)(ys : B【 Γ 】)
→ Rs xs ys → R (λ α → ⟦ t ⟧' α (xs α)) (B⟦ t ⟧ ys)
main-lemma Ω xs ys cr = lemma
where
claim : ∀ α n n' → n α ≡ dialogue n' α → α(n α) ≡ α(decode α n')
claim α n n' s = cong α s
lemma : ∀(n : Baire → ℕ)(n' : B ℕ) → (∀ α → n α ≡ decode α n')
→ ∀ α → α(n α) ≡ decode α (generic n')
lemma n n' rn α = trans (claim α n n' (rn α)) (generic-diagram α n')
main-lemma Zero xs ys cr = λ α → refl
main-lemma Succ xs ys cr = lemma
where
claim : ∀ α n n' → n α ≡ dialogue n' α → succ(n α) ≡ succ(decode α n')
claim α n n' s = cong succ s
lemma : ∀(n : Baire → ℕ)(n' : B ℕ) → (∀ α → n α ≡ decode α n')
→ ∀(α : Baire) → succ (n α) ≡ decode α (B-functor succ n')
lemma n n' rn α = trans (claim α n n' (rn α)) (decode-α-is-natural succ n' α)
main-lemma (Rec {_} {_} {σ}) _ _ _ = lemma
where
lemma : ∀(f : Baire → ℕ → 〖 σ 〗 → 〖 σ 〗)(f' : B ℕ → B〖 σ 〗 → B〖 σ 〗) → R {ι ⇒ σ ⇒ σ} f f'
→ ∀(x : Baire → 〖 σ 〗)(x' : B〖 σ 〗)
→ R {σ} x x' → ∀(n : Baire → ℕ)(n' : B ℕ) → R {ι} n n'
→ R {σ} (λ α → rec (f α) (x α) (n α)) (Kleisli-extension(rec (f' ∘ η) x') n')
lemma f f' rf x x' rx = R-kleisli-lemma σ g g' rg
where
g : ℕ → Baire → 〖 σ 〗
g k α = rec (f α) (x α) k
g' : ℕ → B〖 σ 〗
g' k = rec (f' ∘ η) x' k
rg : ∀(k : ℕ) → R (g k) (g' k)
rg zero = rx
rg (succ k) = rf (λ α → k) (η k) (λ α → refl) (g k) (g' k) (rg k)
main-lemma (ν i) xs ys cr = cr i
main-lemma {n} {Γ} {σ ⇒ τ} (ƛ t) xs ys cr = IH
where
IH : (x : Baire → 〖 σ 〗) (y : B〖 σ 〗)
→ R x y → R (λ α → ⟦ t ⟧' α (xs α ‚ x α)) (B⟦ t ⟧ (ys ‚‚ y))
IH x y r = main-lemma t (λ α → xs α ‚ x α) (ys ‚‚ y) h
where
h : (i : Fin (succ n)) → R (λ α → (xs α ‚ x α) i) ((ys ‚‚ y) i)
h zero = r
h (succ i) = cr i
main-lemma (t · u) xs ys cr = IH-t (λ α → ⟦ u ⟧' α (xs α)) (B⟦ u ⟧ ys) IH-u
where
IH-t : (x : Baire → 〖 _ 〗) (x' : B〖 _ 〗)
→ R x x' → R (λ α → ⟦ t ⟧' α (xs α) (x α)) (B⟦ t ⟧ ys x')
IH-t = main-lemma t xs ys cr
IH-u : R (λ α → ⟦ u ⟧' α (xs α)) (B⟦ u ⟧ ys)
IH-u = main-lemma u xs ys cr
\end{code}
\begin{code}
main-closed-ground : ∀(t : T' 〈〉 ι) (α : Baire) → ⟦ t ⟧' α ⟨⟩ ≡ decode α (B⟦ t ⟧ ⟪⟫)
main-closed-ground t = main-lemma t (λ α → ⟨⟩) ⟪⟫ (λ())
\end{code}
\begin{code}
dialogue-tree-correct : ∀(t : T₀((ι ⇒ ι) ⇒ ι)) (α : Baire) → ⟦ t ⟧₀ α ≡ decode α (dialogue-tree t)
dialogue-tree-correct t α = trans (fact₁ t α) (fact₀ t α)
where
fact₀ : ∀(t : T₀((ι ⇒ ι) ⇒ ι)) (α : Baire) → ⟦ embed t ⟧' α ⟨⟩ α ≡ decode α (dialogue-tree t)
fact₀ t = main-closed-ground((embed t) · Ω)
fact₁ : ∀(t : T₀((ι ⇒ ι) ⇒ ι)) (α : Baire) → ⟦ t ⟧₀ α ≡ ⟦ embed t ⟧' α ⟨⟩ α
fact₁ t α = cong (λ f → f ⟨⟩ α) (preservation t α)
\end{code}
\begin{code}
eloquence-theorem : ∀(f : Baire → ℕ) → T-definable f → eloquent f
eloquence-theorem f (t , r) = (dialogue-tree t , lemma)
where
r' : ∀ α → ⟦ t ⟧ ⟨⟩ α ≡ f α
r' α = cong (λ h → h α) r
lemma : ∀(α : ℕ → ℕ) → dialogue (dialogue-tree t) α ≡ f α
lemma α = trans (sym (dialogue-tree-correct t α)) (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))
\end{code}