In this paper we give a preliminary formalization of the p-adic numbers, in
the context of the second author's univalent foundations program. We also
provide the corresponding code verifying the construction in the proof
assistant Coq. Because work in the univalent setting is ongoing, the structure
and organization of the construction of the p-adic numbers we give in this
paper is expected to change as Coq libraries are more suitably rearranged, and
optimized, by the authors and other researchers in the future. So our
construction here should be deemed as a first approximation which is subject to
improvements.
Description
[1302.1207] A preliminary univalent formalization of the p-adic numbers
%0 Generic
%1 pelayo2013preliminary
%A Pelayo, Álvaro
%A Voevodsky, Vladimir
%A Warren, Michael A.
%D 2013
%K HoTT number
%T A preliminary univalent formalization of the p-adic numbers
%U http://arxiv.org/abs/1302.1207
%X In this paper we give a preliminary formalization of the p-adic numbers, in
the context of the second author's univalent foundations program. We also
provide the corresponding code verifying the construction in the proof
assistant Coq. Because work in the univalent setting is ongoing, the structure
and organization of the construction of the p-adic numbers we give in this
paper is expected to change as Coq libraries are more suitably rearranged, and
optimized, by the authors and other researchers in the future. So our
construction here should be deemed as a first approximation which is subject to
improvements.
@misc{pelayo2013preliminary,
abstract = {In this paper we give a preliminary formalization of the p-adic numbers, in
the context of the second author's univalent foundations program. We also
provide the corresponding code verifying the construction in the proof
assistant Coq. Because work in the univalent setting is ongoing, the structure
and organization of the construction of the p-adic numbers we give in this
paper is expected to change as Coq libraries are more suitably rearranged, and
optimized, by the authors and other researchers in the future. So our
construction here should be deemed as a first approximation which is subject to
improvements.},
added-at = {2015-01-01T07:23:35.000+0100},
author = {Pelayo, Álvaro and Voevodsky, Vladimir and Warren, Michael A.},
biburl = {https://www.bibsonomy.org/bibtex/222306306ef7c5f54b5a3dca150b987e7/t.uemura},
description = {[1302.1207] A preliminary univalent formalization of the p-adic numbers},
interhash = {5147d15138adc9d21fcf696abe1a4ced},
intrahash = {22306306ef7c5f54b5a3dca150b987e7},
keywords = {HoTT number},
note = {cite \href{http://arxiv.org/abs/1302.1207}{arxiv:1302.1207}Comment: 57 pages},
timestamp = {2015-01-01T07:23:35.000+0100},
title = {A preliminary univalent formalization of the p-adic numbers},
url = {http://arxiv.org/abs/1302.1207},
year = 2013
}