by Leandro Caniglia
by Leandro Caniglia
In classical mathematics, a proof is primarily a communication device—a persuasive narrative designed to convince the reader that a particular statement is true. Homotopy Type Theory (HoTT) forces a radical shift in this perspective: a proof is no longer a meta-linguistic explanation but a first-class mathematical object. Specifically, a proof is a function that transforms a witness of the hypotheses into a witness of the thesis.
While this unification of logic and structure is incredibly elegant, it exposes the limits of how we traditionally process mathematical texts.
A persistent illusion when approaching HoTT is that a well-formed mathematical background is sufficient to read its expressions fluently. In classical mathematics, the formalization is adjustable. We rely on natural language stitches—words like “then,” “therefore,” or “it follows that”—to separate hypotheses from conclusions and to embed logical structure within prose.
HoTT tightens these screws. Because proofs are elements of the theory, the required level of detail is naturally higher. The human mind is highly optimized for pattern matching and filling in gaps with imagination, but it is notoriously poor at parsing complex, deeply nested Abstract Syntax Trees (ASTs). When reading a dependent type expression, we must constantly verify the types of the surrounding terms to ensure the expression is well-formed.
For instance, when trying to understand the equivalence of functions, HoTT defines a homotopy $f \sim g$ as a dependent type:
\[ f \sim g :\equiv \prod_{x:A} (f(x) = g(x)) \]
Reading and unpacking these expressions requires keeping track of binders, scopes, and universes. This requirement makes reading HoTT feel less like reading a textbook and more like playing the role of a compiler.
Within this ecosystem, there is a clear division between the mechanical and the intelligent.
The mechanical component operates automatically through rewriting rules (judgmental equality, denoted by $\equiv$). When the system encounters a constructor or a reducible expression, it simplifies it automatically. The mechanical computation stops when it can no longer rewrite the expression.
This is where the intelligent component—the human or the programmer—must step in to provide a theorem (propositional equality, denoted by $=$). We must supply the logical step that tells the machine how to proceed. However, this division contains a trap: when working without a proof assistant, we must perform both the mechanical rewriting and the intelligent deduction ourselves. We quickly discover that our capacity to apply rewriting rules without error degrades rapidly as complexity scales. The cognitive load required to track paths between paths (and paths between those paths) pushes human parsing to its breaking point.
This strict formalization leads to a fascinating distortion: in HoTT, as in Category Theory, the difficulty often shifts from proving the theorems to formulating the definitions and statements correctly.
In traditional mathematics, the statements are usually easy to understand, while the proofs contain the heavy lifting. In HoTT, simply stating a theorem—such as translating a categorical universal property like a pullback into an equivalence of types—requires extreme precision. You must define the correct induction motive and navigate a sea of dependent types and quantifiers.
Once the statement is correctly formulated and the proper abstractions are aligned, the proof itself often reduces to checking types or applying basic path induction. The challenge lies in reaching the point where the obvious actually becomes obvious.
Wrestling with these abstractions is a test of endurance. It is common to spend hours trying to formalize a seemingly trivial property, drowning in 1-paths, 2-paths, and function whiskering, only to hit a wall of overwhelming complexity.
Yet, there is a profound gift in this mental exhaustion. The forced interruption of a tired mind acts as a reset. Often, after going to sleep troubled by an impenetrable diagram or a messy type mismatch, you wake up with a sudden, clarifying vision. The problem reconfigures itself. The convoluted, literal translation of a concept is discarded in favor of a much simpler, more elegant structural equivalence.
Ultimately, HoTT forces a microscopic re-examination of mathematical reasoning. It demands that we formalize the micro-arguments we have culturally learned to gloss over. While the path is incredibly steep and demands a level of rigorous parsing that humbles even experienced readers, the resulting clarity offers a breathtaking view of the foundations of logic.
Studying Homotopy Type Theory is not an easy task. My methodology consists of rewriting the HoTT Book in a more detailed way. Here I share some of the reflections this process has triggered.
Leandro Caniglia