Experimental library of univalent formalization of mathematics
  This paper contains a discussion of a library of formalized mathematics for the proof assistant Coq which the author worked on in 2011-13. 
Vladimir Voevodsky
math.HO math.LO