There are multiple notions of premetrics and premetric spaces in the mathematical literature:
One can also have a distinction between whether one uses the positive rational numbers or the positive real numbers in the premetrics as defined by Booij and by Gilbert, leading to rational premetric spaces and real premetric spaces.
Auke B. Booij: Analysis in univalent type theory [pdf]
Gaëtan Gilbert: Formalising real numbers in homotopy type theory, In: CPP’17, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (2017) 112–124 [doi:10.1145/3018610.3018614]
Lorenzo Molena: A Cubical Path from Algebra to Analysis, talk at TYPES 2026, 8 May 2026 [abstract, slides]
Fred Richman: Real numbers and other completions [pdf]
Simon Henry: Localic Metric spaces and the localic Gelfand duality [arXiv:1411.0898v1]
Last revised on October 5, 2026 at 05:17:35. See the history of this page for a list of all contributions to it.