This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
The mathematical study of type theories, in univalent foundations
This repository makes it easy to build and install UniMath using opam.
A webpage Vladimir made for a conference.
Voevodsky's work on B-systems, transferred from his github account
Voevodsky's work on C-systems, transferred from his github account
A textbook on informal homotopy type theory -- Vladimir's fork, retained because there is a pull request based on it.
Voevodsky's 2006 paper on homotopy lambda calculus
Voevodsky's original development of the univalent foundations of mathematics in Coq
Voevodsky's notes from the summer of 2012 on a design of a universe polymorphic type system with Tarski universes
Voevodsky's notes on type systems. This version contains more material than the one on his website.