## Idea The goal of this line of work is to find an [[nlab:essentially algebraic]] formulation of [[nlab: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 [[nlab:generalized algebraic theory]]; see [[nlab:categorical model of dependent types]] for more information. ## References * Egbert Rijke, _An algebraic formulation of dependent type theory_, [PDF](https://groups.google.com/group/homotopytypetheory/attach/7e6c4f50e3db6d76/presentation.pdf?part=0.1&authuser=0) * Vladimir Voevodsky, _B-systems_, [arXiv](http://arxiv.org/abs/1410.5389) * Vladimir Voevodsky, _A C-system defined by a universe in a category_, [arXiv](http://arxiv.org/abs/1409.7925) * Vladimir Voevodsky, _C-system of a module over a monad on sets_, [arXiv](http://arxiv.org/abs/1407.3394) * Vladimir Voevodsky, _Subsystems and regular quotients of C-systems_, [arXiv](http://arxiv.org/abs/1406.7413)