Homotopy Type Theory algebraic formulation of dependent type theory > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Idea

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.

References

Egbert Rijke, An algebraic formulation of dependent type theory, PDF
Vladimir Voevodsky, B-systems, arXiv
Vladimir Voevodsky, A C-system defined by a universe in a category, arXiv
Vladimir Voevodsky, C-system of a module over a monad on sets, arXiv
Vladimir Voevodsky, Subsystems and regular quotients of C-systems, arXiv

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.