{-# OPTIONS --without-K #-} -- This file guides through how one should read this project module Mint.README where open import Axiom.Extensionality.Propositional -- We only rely on functional extensionality (fext). We use this axiom in -- two places: -- -- 1. Fext is necessary to establish the equality between evaluation environments in -- the domain model. Interestingly, this necessity is introduced because of □ -- modality, i.e. if we formalize ordinary Martin-Löf type theory (MLTT), we would -- not even need fext. Instead of a just keeping tracking of values as in MLTT, we -- also need to keep track of modal offsets in the evaluation environments, thus -- requiring fext. -- -- Use of fext in this case only require functional extensionality at level 0: -- -- Extensionality 0ℓ 0ℓ -- -- 2. Since we are postulating functional extensionality, we might as well abuse it -- a little bit and use it in proving the equality of PER and gluing models for -- universes. This use is not strictly necessary and only require functional -- extensionality at level 1: -- -- Extensionality 1ℓ 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 ℓ ℓ′ -- Syntax, typing rules and equivalence rules import Mint.Statics -- Properties of the syntactic judgments import Mint.Statics.Properties ------------------------------------------------- -- Definitions of Semantics and the NbE algorithm -- Definitions of the untyped semantic domain which the syntax is evaluated to import Mint.Semantics.Domain -- Evaluation from syntactic terms to the domain model import Mint.Semantics.Evaluation -- Read from the domain model back to the syntax as normal/neutral terms import Mint.Semantics.Readback -- PER model for the semantics import Mint.Semantics.PER -- Realizability for the semantics import Mint.Semantics.Realizability ------------------------------------ -- Completeness of the NbE algorithm -- Definitions of semantic judgments for completeness import Mint.Completeness.LogRel -- Fundamental theorems of semantic judgments import Mint.Completeness.Fundamental fext as Fundamental -- Proof of the completeness theorem import Mint.Completeness fext as Completeness -- Consequences of completeness import Mint.Completeness.Consequences fext as Consequence --------------------------------- -- Soundness of the NbE algorithm -- Definitions of the gluing models and semantic judgments for soundness import Mint.Soundness.LogRel -- Realizability for the gluing model import Mint.Soundness.Realizability -- Cumulativity for the gluing model import Mint.Soundness.Cumulativity -- Fundamental theorems of semantic judgments for soundness import Mint.Soundness.Fundamental fext as Fundamental′ -- Proof of the soundness theorem import Mint.Soundness fext as Soundness --------------------------------- -- Consequences of soundness import Mint.Consequences fext as Consequence′