<<<<<<< HEAD
Internal models of type theory.
The goal of this project is to give a definition of internal models of type theory and their morphisms which has been set up in such a way that any choice of the type constructors can be left out if that is desired. The output of the project is a document containing all the ideas that go into the definition. Apart from the definition of internal models itself we also explore:
- examples of internal models together with their properties.
- variations to the syntax.
- properties of the class of all internal models and their morphisms.
- properties of other classes of internal models (e.g. those for which all morphisms are invertible).
The document article-models-main.tex is the main document. It compiles with TeXlive 2012 or later versions thereof.
e-systems
E-systems
04878af28f55cef4e6505cc65980aff63466c049