Report or block vladimirias
Contact Support about this user's behavior.Report abuse
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
A textbook on informal homotopy type theory
Development of the univalent foundations of mathematics in Coq
My notes fro the summer of 2012 on a design of a universe polymorphic type system with Tarski universes
Notes on type systems. This version contains more material than the one on my website.