/-- **The interpretation of terms as morphisms** `⟦Γ⟧ → ⟦A⟧` of the cartesian closed category
of types: pairing is the map into a product, `fst`/`snd` compose with projections, `lam` is
**currying** (the bijection `Hom(Γ × A, B) ≅ Hom(Γ, B^A)`), and `app` composes with
**evaluation** `B^A × A → B`. -/
def Tm.denote {X : Type} : {Γ : List Ty} → {A : Ty} → Tm Γ A → ctxDenote X Γ → A.denote X
| _, _, .var v, γ => v.denote γ
| _, _, .star, _ => ()
| _, _, .pair s t, γ => (s.denote γ, t.denote γ)
| _, _, .fst t, γ => (t.denote γ).1
| _, _, .snd t, γ => (t.denote γ).2
| _, _, .lam t, γ => fun a => t.denote (a, γ)
| _, _, .app s t, γ => s.denote γ (t.denote γ)