natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Given a (dependent) type theory, then its term model is a model which consists of exactly those types and terms which may be constructed (via the relevant natural deduction operations) in the type theory.
The term model is supposed to be is the initial object in the category of all models of the given type theory.
e.g. Hofmann, example 1
Under the relation between type theory and category theory the term model is a category, essentially the syntactic category of the type theory.
Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories (pdf)
Alexandre Buisse, Peter Dybjer, Towards Formalizing Categorical Models of Type Theory in Type Theory, 2007 (pdf)
Peter Aczel, What is a type theory and what should a type theory be?, 2012 (pdf, pdf)
Last revised on February 1, 2015 at 23:20:36. See the history of this page for a list of all contributions to it.