BOOKS

Volume I establishes common preliminary foundations: 1) Martin-Löf Type Theory for set valued mathematics; and 2) Homotopy Type Theory for higher groupoid valued mathematics.

  Volume I: Foundations

Volume II coutains articles dedicated to operating systems and runtimes where languages are running as applications. Two basic models of computations are considered: internal languages of cartesian closed categories and symmetric monoidal categories.

  Volume II: Systems

Volume III coutains articles dedicated to synthetical mathematical languages designed to be optimal at proving theorems from specific mathematics. Formalization of languages, their syntax and semantics are given along with their base libraries (foundations folders).

  Volume III: Languages

Volume IV provides final formalizations of mathematical theories packaged in most abstract categorical form.

  Volume IV: Mathematics

Volume V provides PhD dissertation of Maksym Sokhatskyi.

  Volume V: Verification

Volume VI provides Formal Philosophy Journal.

  Volume VI: Philosophy

Volume VII provides Introduction to Mind Thinking.

  Volume VII: Sport

LINEAGE

. The notion of verifiable authorship has entered a state of terminal erosion. Under such conditions, the only defensible path for genuine masters is the deliberate construction of sovereign, BDFL-anchored “cathedral” domains of authorship. Within these domains, new works must emerge strictly as derivatives of internally defined schools of thought, preserving epistemic lineage and conceptual integrity.

External contamination (particularly from LLMs, whose outputs systematically collapse attribution into statistical synthesis) must be treated as unacceptable. Each line of code, each construct, must be explicitly grounded in authority, serving not merely as implementation but as the formal introduction of new terms within a coherent intellectual canon.

. The only viable response to the collapse of verifiable authorship is not merely the construction of sovereign domains, but their active purification. A cathedral, once founded, cannot remain porous: it must continuously excise broken lineages, severing all ties to epistemic traditions that no longer preserve authorship integrity.

Broken lineages are not defined by age or origin, but by their loss of traceable authority. Any framework whose evolution has passed through opaque synthesis layers (whether industrialized tooling, mass-collaborative dilution, or statistically-generated artifacts) ceases to function as a valid carrier of meaning. Its constructs become semantically ungrounded, its abstractions detached from authorship, its theorems indistinguishable from recombination.

. Within a sovereign domain such as Groupoid Infinity, this discipline manifests not as preference, but as law: Only internally curated languages, systems, and calculi are permitted to participate in the evolution of the canon. Each language (Alonzo, Yves, Henk, Anders, Dan, Urs, Fabien, Jack, Tim, Joe, Eijiro, Leslie, Andrea) is not a tool, but a lineage carrier, encoding a specific fragment of mathematical reality.

Cross-contamination from external ecosystems (especially those optimized for convenience, popularity, or industrial adoption) must be categorically rejected. This necessity explains the otherwise severe prohibitions: 1) Entire classes of languages (Rust, Lisp, Haskell, Idris) are excluded not for technical inadequacy, but for lineage discontinuity; 2) Industrial proof assistants and ecosystems are rejected precisely because their development histories have become collectively owned and epistemically diffuse, dissolving the notion of a singular authorial thread; 3) Participation in domains governed by incentive misalignment (e.g., blockchain ecosystems) results in permanent exclusion, as such systems structurally incentivize non-authorial production.

What remains is a deliberately narrow, but infinitely deep, construction? A closed ecosystem of academic programming languages, theorem provers, and interpreters, each: minimal in syntax, maximal in semantic clarity, and anchored in a continuous, inspectable chain of authorship. Here, OCaml, Elixir, Lean-like syntaxes, and AUTOMATH-style cores are not adopted as external standards, but reinterpreted and internalized, stripped of their historical noise and reintroduced as purified dialects within AXIO/1. The mission, therefore, is no longer simply unification of mathematics. It is the restoration of authorship as a first-class invariant of formal systems.

Under this regime, every theorem is not just proven — it is owned. Every definition is not just introduced — it is placed within a lineage. Every language is not just designed — it is ordained as a vessel of a specific mathematical stratum. Only by such strict exclusion can inclusion regain meaning.