Click here to flash read.
It is well-known that simple type theory is complete with respect to
non-standard set-valued models. Completeness for standard models only holds
with respect to certain extended classes of models, e.g., the class of
cartesian closed categories. Similarly, dependent type theory is complete for
locally cartesian closed categories. However, it is usually difficult to
establish the coherence of interpretations of dependent type theory, i.e., to
show that the interpretations of equal expressions are indeed equal. Several
classes of models have been used to remedy this problem. We contribute to this
investigation by giving a semantics that is standard, coherent, and
sufficiently general for completeness while remaining relatively easy to
compute with. Our models interpret types of Martin-L\"of's extensional
dependent type theory as sets indexed over posets or, equivalently, as
fibrations over posets. This semantics can be seen as a generalization to
dependent type theory of the interpretation of intuitionistic first-order logic
in Kripke models. This yields a simple coherent model theory, with respect to
which simple and dependent type theory are sound and complete.
No creative common's license