Showing changes from revision #1 to #2:
Added | Removed | Changed
The goal of this line of work is to find algebraic an formulations ofessentially algebraic formulation of dependent type theory . This automatically provides free models and quotients. The syntax will then be the initial model.
Rijke’s E-systems are a generalization of Voevodsky’s B-systems.
This line of research should be compared with Dybjer’s categories with families which is a generalized algebraic theory; see categorical model of dependent types for more information.
Revision on March 15, 2015 at 00:37:33 by Bas Spitters. See the history of this page for a list of all contributions to it.