Segment or loop? A homotopy-type-theoretic overview of the dispute over Corollary 3.12 of inter-universal Teichmüller theory

The dispute over Corollary 3.12 of inter-universal Teichmüller theory (IUT) III has been conducted in many vocabularies: the identification and the labelling of isomorphic copies; monodromy; segment, loop and universal cover; multiradiality and the properties IPL, SHE and APT; logical AND and logical OR; descent; commutativity up to indeterminacies; the size of the blurring. This paper shows that these become precise propositions in one language, that of homotopy type theory (types, paths, transport, truncation, families over graphs), and that the location of the dispute is then fixed at a single point. There are five main results. (A) Identifying isomorphic copies along a single path loses no information. (B) If two stages are joined by two paths, a family over them is equivalent to a family over a loop, and the composite of the two paths (the monodromy) is a complete invariant; if it is nontrivial, the only value that is single-valued on the loop is 0. (C) Corollary 3.12 is equivalent to a lax 2-cell between the two paths: a single inequality saying that the blurring by the indeterminacies absorbs the discrepancy of the monodromy, which itself has the shape of an upper bound for a height; together with the upper bound for the blurring in IV, it gives a height bound. (D) If the blurring is taken along the whole loop, the hull becomes trivial and the inequality says nothing. (E) IPL, SHE and APT are one-dimensional data (paths and functoriality) and are compatible with any size of the blurring, so neither Corollary 3.12 nor its negation follows from them. One level down, for presented reals and Booij's locators, there is no monodromy and the blurring of the possible images is uniformly bounded; the difference is a difference of h-level. None of the results is new mathematically; the contribution is the formulation that places known mathematics in one framework, and the correspondence with the vocabulary of each party. Each statement is labelled as a quotation, a claim of another author, a proposition, a formulation of known mathematics (with its source), or a reading. The quantitative core is checked in Lean 4. Nothing is claimed about the truth of Corollary 3.12, Theorem 1.10 of IUT IV, or the abc conjecture. A companion note in undergraduate mathematics is doi:10.5281/zenodo.23931346. This is a preprint. Use of generative AI. The idea of this paper (to survey the dispute in the language of homotopy type theory) is the author's. Generative AI tools (large language models) were used extensively, under the author's direction, in writing the text and the proofs and in the verification in Lean. The author takes full responsibility for the contents of this paper. The deposit contains the paper and an archive of the folder segment-or-loop/ (the LaTeX source, the Lean file with its project files, and the output of #print axioms), made from tag v0.13.0 of github.com/turahigashi/iut-explicit-initial-theta. The files are licensed under CC BY 4.0.