This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Formalization of p-adic numbers, described in

Álvaro Pelayo, Vladimir Voevodsky, and Michael A. Warren A univalent formalization of the p-adic numbers Math. Struct. in Comp. Science (2015), vol. 25, pp. 1147–1171. doi:10.1017/S0960129514000541

Also see Álvaro Pelayo, Vladimir Voevodsky and Michael A. Warren, A preliminary univalent formalization of the p-adic numbers at arXiv.

*fps.v*— formal power series, only based on lemmas.v*frac.v*— fractions, only based on lemmas.v*lemmas.v*— preparations, needed for all other files*padics.v*— the p-adic numbers, needs all other files*z_mod_p.v*— integers mod p, only based on lemmas.v