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


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


  • 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

Revision on March 14, 2015 at 17:26:33 by Bas Spitters. See the history of this page for a list of all contributions to it.