{-# OPTIONS --without-K --safe #-} -- A special set of typing rules just for soundness (the Sound formulation) -- -- It appears that to establish the soundness proof, we need a bit strengthening of -- induction hypothesis in the fundamental theorems, particularly in Λ-E and □-E -- case. This set of rules only adds to the Concise formulation two premises. This set -- of rules are defined to expose this strengthening and the added premises are marked -- by -- -- -- expose typing judgments for soundness proof -- -- We then can show this formulation and the Concise formulation (i.e. the golden -- formulation) is equivalent (actually we just need one directly), -- c.f. MLTT.Soundness.Equiv for the proof. module MLTT.Soundness.Typing where open import Lib open import MLTT.Statics.Syntax public import MLTT.Statics.Concise as C infix 4 ⊢_ _⊢_∶_ _⊢s_∶_ mutual data ⊢_ : Ctx → Set where ⊢[] : ⊢ [] ⊢∷ : ∀ {i} → ⊢ Γ → Γ ⊢ T ∶ Se i → -------------- ⊢ T ∷ Γ data _⊢_∶_ : Ctx → Exp → Typ → Set where N-wf : ∀ i → ⊢ Γ → ------------- Γ ⊢ N ∶ Se i Se-wf : ∀ i → ⊢ Γ → ---------------- Γ ⊢ Se i ∶ Se (1 + i) Π-wf : ∀ {i} → Γ ⊢ S ∶ Se i → S ∷ Γ ⊢ T ∶ Se i → -------------------- Γ ⊢ Π S T ∶ Se i vlookup : ∀ {x} → ⊢ Γ → x ∶ T ∈! Γ → ------------ Γ ⊢ v x ∶ T ze-I : ⊢ Γ → ----------- Γ ⊢ ze ∶ N su-I : Γ ⊢ t ∶ N → ------------- Γ ⊢ su t ∶ N N-E : ∀ {i} → N ∷ Γ ⊢ T ∶ Se i → Γ ⊢ s ∶ T [| ze ] → T ∷ N ∷ Γ ⊢ r ∶ T [ (wk ∘ wk) , su (v 1) ] → Γ ⊢ t ∶ N → -------------------------- Γ ⊢ rec T s r t ∶ T [| t ] Λ-I : S ∷ Γ ⊢ t ∶ T → ------------------ Γ ⊢ Λ t ∶ Π S T Λ-E : ∀ {i} → -- expose typing judgments for soundness proof S ∷ Γ ⊢ T ∶ Se i → Γ ⊢ r ∶ Π S T → Γ ⊢ s ∶ S → --------------------- Γ ⊢ r $ s ∶ T [| s ] t[σ] : Δ ⊢ t ∶ T → Γ ⊢s σ ∶ Δ → --------------------- Γ ⊢ t [ σ ] ∶ T [ σ ] cumu : ∀ {i} → Γ ⊢ T ∶ Se i → ------------------ Γ ⊢ T ∶ Se (1 + i) conv : ∀ {i} → Γ ⊢ t ∶ S → Γ C.⊢ S ≈ T ∶ Se i → ------------------ Γ ⊢ t ∶ T data _⊢s_∶_ : Ctx → Subst → Ctx → Set where s-I : ⊢ Γ → ------------ Γ ⊢s I ∶ Γ s-wk : ⊢ T ∷ Γ → ------------------ T ∷ Γ ⊢s wk ∶ Γ s-∘ : Γ ⊢s τ ∶ Γ′ → Γ′ ⊢s σ ∶ Γ″ → ---------------- Γ ⊢s σ ∘ τ ∶ Γ″ s-, : ∀ {i} → Γ ⊢s σ ∶ Δ → Δ ⊢ T ∶ Se i → Γ ⊢ t ∶ T [ σ ] → ------------------- Γ ⊢s σ , t ∶ T ∷ Δ s-conv : Γ ⊢s σ ∶ Δ → C.⊢ Δ ≈ Δ′ → ------------- Γ ⊢s σ ∶ Δ′