@article{PELAYO_2015,
    doi = {10.1017/s0960129514000541},
    url = {https://doi.org/10.1017%2Fs0960129514000541},
    year = {2015},
    month = {feb},
    publisher = {Cambridge University Press ({CUP})},
    volume = {25},
    number = {5},
    pages = {1147--1171},
    author = {{\'{A}}LVARO PELAYO and VLADIMIR VOEVODSKY and MICHAEL A. WARREN},
    title = {A univalent formalization of the -adic numbers},
    journal = {Mathematical Structures in Computer Science}
}

@article{PELAYO_2015, doi = {10.1017/s0960129514000541}, url = {https://doi.org/10.1017%2Fs0960129514000541}, year = {2015}, month = {feb}, publisher = {Cambridge University Press ({CUP})}, volume = {25}, number = {5}, pages = {1147--1171}, author = {{\'{A}}LVARO PELAYO and VLADIMIR VOEVODSKY and MICHAEL A. WARREN}, title = {A univalent formalization of the -adic numbers}, journal = {Mathematical Structures in Computer Science} }