An experimental library of formalized Mathematics based on the univalent foundations

Luo, 1994, Computation and Reasoning. A Type Theory for Computer Science, 10.1093/oso/9780198538356.001.0001

Ahrens B. , Kapulkin C. and Shulman M. (2014) Univalent categories and the Rezk completion. Mathematical Structures in Computer Science http://dx.doi.org/10.1017/S0960129514000486.

Makkai M. (1995) First order logic with dependent sorts, with applications to category theory. Preprint, Available at: http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf.

Paulin-Mohring C. (1993) Inductive definitions in the system Coq: Rules and properties. In: Typed Lambda Calculi and Applications (Utrecht, 1993), Springer Lecture Notes in Computer Science volume 664 Berlin 328–345.

Grothendieck, 1997, Geometric Galois Actions, 1, 5

Kapulkin C. , LeFanu Lumsdaine P. and Voevodsky V. (2012) The simplicial model of univalent foundations. Preprint, arXiv:1211.2851.

10.1016/0890-5401(88)90005-3

Univalent Foundations Project (2013) Homotopy type theory: Univalent foundations for mathematics. Available at: http://homotopytypetheory.org/book.

Pelayo A. , Voevodsky V. and Warren M. A. (2014) A preliminary univalent formalization of the p-adic numbers. Mathematical Structures in Computer Science http://dx.doi.org/10.1017/S0960129514000541.

Voevodsky V. (2011) Resizing rules, slides from a talk at TYPES2011. Available at: https://github.com/vladimirias/2011_Bergen.