Homotopy Type Theory algebraic formulation of dependent type theory > history (Rev #1)

Idea

The goal of this line of work is to find algebraic formulations of dependent type theory. The syntax will then be the initial model.

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