#
Homotopy Type Theory

algebraic formulation of dependent type theory (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

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.