algebraic formulation of dependent type theory (Rev #3, changes)

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

The goal of this line of work is to find an essentially 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.

~~Egbert~~~~Rijke,~~*An algebraic formulation of dependent type theory*Egbert Rijke,

*An algebraic formulation of dependent type theory*, PDF~~,~~~~PDF~~~~Vladimir~~~~Voevodsky,~~*B-systems*Vladimir Voevodsky,

*B-systems*, arXiv~~,~~~~arXiv~~~~Vladimir~~~~Voevodsky,~~*A C-system defined by a universe in a category*Vladimir Voevodsky,

*A C-system defined by a universe in a category*, arXiv~~,~~~~arXiv~~~~Vladimir~~~~Voevodsky,~~*C-system of a module over a monad on sets*Vladimir Voevodsky,

*C-system of a module over a monad on sets*, arXiv~~,~~~~arXiv~~~~Vladimir~~~~Voevodsky,~~*Subsystems and regular quotients of C-systems*Vladimir Voevodsky,

*Subsystems and regular quotients of C-systems*, arXiv~~,~~~~arXiv~~

Revision on October 10, 2018 at 09:36:35 by Ali Caglayan. See the history of this page for a list of all contributions to it.