A univalent formalization of the <i>p</i>-adic numbers
A univalent formalization of the <i>p</i>-adic numbers
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.