{-# OPTIONS --without-K #-} open import MLTT.Spartan hiding (Π; zero; succ) open import UF.FunExt open import ag-000V open import ag-000W module ag-000Y (fe : Fun-Ext) where
A model mapping TT to untyped lambda calculus.
module LC-TT {𝓤 𝓥 : Universe} (l : LC {𝓥}) where open LC open TT open TT-sorts open TT-ctors ex-sorts : TT-sorts {𝓤} {𝓥} ex-sorts .Ty = 𝟙 ex-sorts .Tm _ = l .Λ ex-ctors : TT-ctors ex-sorts ex-ctors .Π A B = ⋆ ex-ctors .lam f = l .lambda f ex-ctors .app f x = l .apply f x ex-ctors .lam-app = l .η _ ex-ctors .app-lam {a}{b}{f} = (λ x → l .apply (l .lambda f) x) ＝⟨ dfunext fe (λ x → l .β f x) ⟩ (λ x → f x) ＝⟨ refl ⟩ f ∎ ex-ctors .U = ⋆ ex-ctors .El _ = ⋆ ex-ctors .Nat = ⋆ ex-ctors .zero = zeroΛ l ex-ctors .succ x = succΛ l x ex-ctors .elim-Nat X ze su n = recΛ l ze su n ex-ctors .elim-Nat-zero = recΛβ-zero l ex-ctors .elim-Nat-succ = recΛβ-succ l ex : TT {𝓤} {𝓥} ex .sorts = ex-sorts ex .ctors = ex-ctors