We propose a formalization of the concept of the infinium — the minimal structural quantum underlying △-ontology — in the language of dependent type theory. The infinium is introduced as a signature satisfying three axioms: irreflexivity of orthogonality, the Pythagorean theorem for an internal measure, and self-similarity (cutting along the altitude). We show how natural, integer, rational, real, and complex numbers are constructively built from this signature, as well as a topos of sheaves on a site of finite approximations that serves as a universe for all of mathematics. Explicit signatures and axioms at each level are given, together with the formulation of the main forcing statement.
Alexey (KAMAZ) Petrov (Wed,) studied this question.