module Semantics.TypingJudgments where open import IType.Nat open import Semantics.SyntaxComputationRulesITT data isN : F zero → Set where zeroN : {a : F zero} → a => zeroV → isN a succN : {a b : F zero} → a => succV b → isN b → isN a -- an inductive-recursive definition! mutual data isset : F zero → Set where piset : {A : F zero} → (B : F zero) → (C : F one) → A => piV B C → (p : isset B) → ((x : F zero) → isel x B p → isset (C [ x ])) → isset A Nset : {A : F zero} → A => NV → isset A isel : F zero → (A : F zero) → isset A → Set isel a A (piset B C d p q) = (x : F zero) → (y : isel x B p) → isel (a # x) (C [ x ]) (q x y) isel a A (Nset x) = isN a mutual data isTy : F zero → Set where piTy : {A : F zero} → (B : F zero) → (C : F one) → A => piV B C → (p : isTy B) → ((x : F zero) → isTm x B p → isTy (C [ x ])) → isTy A setTy : {A : F zero} → A => setV → isTy A NTy : {A : F zero} → A => NV → isTy A isTm : F zero → (A : F zero) → isTy A → Set isTm a A (piTy B C d p q) = (b : F zero) → (y : isTm b B p) → isTm (a # b) (C [ b ]) (q b y) isTm a A (setTy x) = isset a isTm a A (NTy x) = isN a -- Meaning of hypothetical judgments. -- The meaning x : A ⊢ b : B is the same as the meaning of -- λ x → b : (x : A) → B, etc -- The meaning of x : A ⊢ B is? -- Exercise: extend the model with more types, e g Bool, Sigma, +, W, -- Exercise: write meanings of equality judgments -- Exercise: write meanings of the identity type