{-# OPTIONS --without-K #-} -- This file guides through how one should read this project module MLTT.README where open import Level open import Axiom.Extensionality.Propositional -- We only rely on functional extensionality (fext). We use this axiom to prove the -- equality of PER and gluing models for universes. This use is not strictly -- necessary and only require functional extensionality at level 1: -- -- Extensionality 0ℓ 1ℓ -- -- In this mechanization, all concepts are defined without fext. For properties of -- semantics that do not require fext, we place them in Properties.NoFunExt. postulate fext : Extensionality 0ℓ (suc 0ℓ) -- Syntax, typing rules and equivalence rules import MLTT.Statics -- Properties of the syntactic judgments import MLTT.Statics.Properties ------------------------------------------------- -- Definitions of Semantics and the NbE algorithm -- Definitions of the untyped semantic domain which the syntax is evaluated to import MLTT.Semantics.Domain -- Evaluation from syntactic terms to the domain model import MLTT.Semantics.Evaluation -- Read from the domain model back to the syntax as normal/neutral terms import MLTT.Semantics.Readback -- PER model for the semantics import MLTT.Semantics.PER -- Realizability for the semantics import MLTT.Semantics.Realizability ------------------------------------ -- Completeness of the NbE algorithm -- Definitions of semantic judgments for completeness import MLTT.Completeness.LogRel -- Fundamental theorems of semantic judgments import MLTT.Completeness.Fundamental fext as Fundamental -- Proof of the completeness theorem import MLTT.Completeness fext as Completeness -- Consequences of completeness import MLTT.Completeness.Consequences fext as Consequence --------------------------------- -- Soundness of the NbE algorithm -- Definitions of the gluing models and semantic judgments for soundness import MLTT.Soundness.LogRel -- Realizability for the gluing model import MLTT.Soundness.Realizability -- Cumulativity for the gluing model import MLTT.Soundness.Cumulativity -- Fundamental theorems of semantic judgments for soundness import MLTT.Soundness.Fundamental fext as Fundamental′ -- Proof of the soundness theorem import MLTT.Soundness fext as Soundness --------------------------------- -- Consequences of soundness import MLTT.Consequences fext as Consequence′