{-# OPTIONS --safe --without-K #-} module ag-0005 where open import MLTT.Spartan
record lambda-calculus : 𝓤₁ ̇ where field Tm : 𝓤₀ ̇
lam 的（metatheory）型別不是一階的（not strictly
positive）
lam : (Tm → Tm) → Tm _·_ : Tm → Tm → Tm β : {f : Tm → Tm} {u : Tm} → lam f · u ＝ f u infixl 30 _·_
By the syntax of lambda calculus, we mean the syntax for the GAT of Definition 4. However, we still prefer to define lambda calculus as a SOGAT: it is a shorter definition, does not include boilerplate, and ensures that once translated to its first-order version, all operations respect substitution by construction.
此外，我們可以像邏輯框架一樣，使用二階表示來進行程式設計。這意味著，使用二階表示，我們可以定義 derivable operation 並證明 derivable 等式，而不是像證明 admissible 那樣需要歸納法。
舉例來說 Y combinator 是 derivable operation。可以證明它是 fixpoint combinator：
Y : Tm Y = lam (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) Y-is-fixed-point : {f : Tm} → Y · f ＝ f · (Y · f) Y-is-fixed-point {f} = Y · f ＝⟨by-definition⟩ lam (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) · f ＝⟨ β ⟩ (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) f ＝⟨ refl ⟩ (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x))) ＝⟨ β ⟩ f · ((lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) ＝⟨ refl ⟩ f · ((λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) f) ＝⟨ ap (f ·_) (β ⁻¹) ⟩ f · (Y · f) ∎
這種推理對任何 second-order model 都有效，而且任何 first-order model 都可以在 internal language of presheaves over first-order model 裡被升級成 second-order model。