@article {37, title = {A univalent formalization of the p-adic numbers}, journal = {Mathematical Structures in Computer Science}, volume = {FirstView}, year = {2015}, note = {

The arXiv version is here.

}, month = {2}, pages = {1{\textendash}25}, issn = {1469-8072}, doi = {10.1017/S0960129514000541}, url = {http://journals.cambridge.org/article_S0960129514000541}, author = {Pelayo, {\'A}lvaro and Voevodsky, Vladimir and Warren, Michael A.} }