Univalent Semantics of Constructive Type Theories. - Vladimir Voevodsky (CPP, 2011)

Univalent Foundations of Mathematics. - Vladimir Voevodsky (WoLLIC, 2011)

A preliminary univalent formalization of the p-adic numbers - Álvaro Pelayo; Vladimir Voevodsky; Michael A. Warren (CoRR, 2013)

A univalent formalization of the p-adic numbers. - Álvaro Pelayo; Vladimir Voevodsky; Michael A. Warren (Math. Struct. Comput. Sci., 2015)

An experimental library of formalized Mathematics based on the univalent foundations. - Vladimir Voevodsky (Math. Struct. Comput. Sci., 2015)

Categorical structures for type theory in univalent foundations. - Benedikt Ahrens; Peter LeFanu Lumsdaine; Vladimir Voevodsky (Log. Methods Comput. Sci., 2018)