## Idea The goal of this line of work is to find algebraic formulations of [[nlab:dependent type theory]]. The syntax will then be the initial model. ## 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)