SOGAT of untyped lambda calculus

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan hiding (id)
open import ag-0005

module ag-000V where

SOGAT of untyped lambda calculus.

record LC : 𝓤 ⁺  ̇ where
  field
    Λ : 𝓤 ̇
    lambda : (f : Λ → Λ) → Λ
    apply : Λ → Λ → Λ
    β : ∀ f x → apply (lambda f) x ＝ f x
    η : ∀ f → lambda (λ x → apply f x) ＝ f

  _$_ : Λ → Λ → Λ
  x $ y = apply x y
  infixl 30 _$_

  syntax lambda (λ x → t) = ƛ x ⇒ t

  zeroΛ : Λ
  zeroΛ = ƛ z ⇒ ƛ s ⇒ z

  succΛ : Λ → Λ
  succΛ n = ƛ z ⇒ ƛ s ⇒ (s $ n $ (n $ z $ s))

  id : Λ
  id = ƛ x ⇒ x

  recΛ : Λ → (Λ → Λ → Λ) → Λ → Λ
  recΛ zr su n = n $ zr $ (ƛ k ⇒ ƛ sk ⇒ su k sk)

  recΛβ-zero : ∀ {zr su} → recΛ zr su zeroΛ ＝ zr
  recΛβ-zero {zr} {su} =
    (ap (_$ (ƛ k ⇒ ƛ sk ⇒ su k sk)) (β (λ z → ƛ s ⇒ z) zr))
    ∙ (β (λ _ → zr) (ƛ k ⇒ ƛ sk ⇒ su k sk))

  recΛβ-succ : ∀ {zr su n} → recΛ zr su (succΛ n) ＝ su n (recΛ zr su n)
  recΛβ-succ {zr} {su} {n} =
    (ap (_$ (ƛ k ⇒ ƛ sk ⇒ su k sk)) (β (λ z → ƛ s ⇒ (s $ n $ (n $ z $ s))) zr))
    ∙ (β (λ s → s $ n $ (n $ zr $ s)) (ƛ k ⇒ ƛ sk ⇒ su k sk))
    ∙ (ap (_$ (n $ zr $ (ƛ k ⇒ ƛ sk ⇒ su k sk))) (β (λ k → ƛ sk ⇒ su k sk) n))
    ∙ (β (λ sk → su n sk) (n $ zr $ (ƛ k ⇒ ƛ sk ⇒ su k sk)))

  embed-nat : ℕ → Λ
  embed-nat 0 = zeroΛ
  embed-nat (succ x) = succΛ (embed-nat x)

Lambda calculus (Second-order algebraic theories) universe polymorphic extended.

SOGAT of untyped lambda calculus [ag-000V]