```module HOAS.SimplyTyped where

infixl 70 _·_
infix  50 ƛ_
infixr 30 _⟶_

data Ty : Set where
base : Ty
_⟶_  : (σ τ : Ty) → Ty

data Tm' (V : Ty → Set) : Ty → Set where
var : ∀ {σ}   (x : V σ) → Tm' V σ
ƛ_  : ∀ {σ τ} (t : V σ → Tm' V τ) → Tm' V (σ ⟶ τ)
_·_ : ∀ {σ τ} (t₁ : Tm' V (σ ⟶ τ)) (t₂ : Tm' V σ) → Tm' V τ

Tm : Ty → Set1
Tm σ = ∀ {V} → Tm' V σ

Val' : (Ty → Set) → Ty → Set
Val' B base    = B base
Val' B (σ ⟶ τ) = Val' B σ → Val' B τ

Val : Ty → Set1
Val σ = ∀ {V} → Val' V σ

⟦_⟧' : ∀ {B τ} → Tm' (Val' B) τ → Val' B τ
⟦ var x   ⟧' = x
⟦ ƛ t     ⟧' = λ x → ⟦ t x ⟧'
⟦ t₁ · t₂ ⟧' = ⟦ t₁ ⟧' ⟦ t₂ ⟧'

⟦_⟧ : ∀ {τ} → Tm τ → Val τ
⟦ t ⟧ = ⟦ t ⟧'

mutual

data Ne' (V : Ty → Set) : Ty → Set where
var : ∀ {τ} (x : V τ) → Ne' V τ
_·_ : ∀ {σ τ} (t₁ : Ne' V (σ ⟶ τ)) (t₂ : NF' V σ) → Ne' V τ

data NF' (V : Ty → Set) : Ty → Set where
ne : (t : Ne' V base) → NF' V base
ƛ_ : ∀ {σ τ} (t : V σ → NF' V τ) → NF' V (σ ⟶ τ)

NF : Ty → Set1
NF σ = ∀ {V} → NF' V σ

mutual

reflect : ∀ {V} τ → Ne' V τ → Val' (Ne' V) τ
reflect base    t = t
reflect (σ ⟶ τ) t = λ v → reflect τ (t · reify σ v)

reify : ∀ {V} τ → Val' (Ne' V) τ → NF' V τ
reify base    t = ne t
reify (σ ⟶ τ) f = ƛ (λ x → reify τ (f (reflect σ (var x))))

nf : ∀ {τ} → Tm τ → NF τ
nf t = reify _ ⟦ t ⟧
```