A univalent formalization of the p-adic numbers
From MaRDI portal
Publication:5740654
DOI10.1017/S0960129514000541zbMath1361.68190arXiv1302.1207OpenAlexW2171238335MaRDI QIDQ5740654
Á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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Vladimir Aleksandrovich Voevodsky ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ On Small Types in Univalent Foundations ⋮ Hamiltonian and symplectic symmetries: An introduction
Uses Software
Cites Work
- Constructing integrable systems of semitoric type
- 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
- Convexity properties of the moment mapping
- A course in constructive algebra
- Homotopy type theory and Voevodsky’s univalent foundations
- Voevodsky’s Univalence Axiom in Homotopy Type Theory
- Convexity and Commuting Hamiltonians
- Type Theory and Homotopy
- Unnamed Item
- Unnamed Item
This page was built for publication: A univalent formalization of the p-adic numbers
