A univalent formalization of the p-adic numbers

作者：Pelayo Alvaro^*; Voevodsky Vladimir; Warren Michael A

来源：Mathematical Structures in Computer Science, 2015, 25(5): 1147-1171.

DOI：10.1017/S0960129514000541

The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.

• 出版日期2015-6