A univalent formalization of the p-adic numbers

DOI10.1017/S0960129514000541MaRDI QIDQ5740654zbMATH OpenOpenAlexFDO

Authors Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren

Publication date 27 July 2016

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1302.1207

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Other constructive mathematics (03F65) Other analytic theory (analogues of beta and gamma functions, (p)-adic integration, etc.) (11S80)

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.

Recommendations

• A transfer theorem in constructive \(p\)-adic algebra
• An experimental library of formalized mathematics based on the univalent foundations
• scientific article; zbMATH DE number 4125509
• scientific article; zbMATH DE number 4040146
• Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers

Cites work

• A course in constructive algebra
• Constructing integrable systems of semitoric type
• Convexity and Commuting Hamiltonians
• Convexity properties of the moment mapping
• Homotopy type theory and Voevodsky's univalent foundations
• scientific article; zbMATH DE number 3880972 (Why is no real title available?)
• scientific article; zbMATH DE number 4002093 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Semitoric integrable systems on symplectic 4-manifolds
• Type theory and homotopy
• Voevodsky’s Univalence Axiom in Homotopy Type Theory

Cited in

(10)

• A transfer theorem in constructive \(p\)-adic algebra
• Homotopy type theory and Voevodsky's univalent foundations
• scientific article; zbMATH DE number 4040146 (Why is no real title available?)
• scientific article; zbMATH DE number 4125509 (Why is no real title available?)
• Vladimir Aleksandrovich Voevodsky
• Hamiltonian and symplectic symmetries: an introduction
• scientific article; zbMATH DE number 5035435 (Why is no real title available?)
• On Small Types in Univalent Foundations
• The p-adic Jaynes-Cummings model in symplectic geometry
• A formalization of divided powers in lean

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A univalent formalization of the \(p\)-adic numbers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740654)