## 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_, ([mailing list discussion](https://groups.google.com/forum/#!topic/homotopytypetheory/OraMqbnCYy8/discussion)) * Vladimir Voevodsky, _B-systems_, [arXiv](http://arxiv.org/abs/1410.5389) * Vladimir Voevodsky, _A C-system defined by a universe in a category_, [arXiv:1406.7413](http://arxiv.org/abs/1409.7925) * Vladimir Voevodsky, _C-system of a module over a monad on sets_, [arXiv:1406.7413](http://arxiv.org/abs/1407.3394) * Vladimir Voevodsky, _Subsystems and regular quotients of C-systems_, [arXiv:1406.7413](http://arxiv.org/abs/1406.7413)