by Leandro Caniglia
by Leandro Caniglia
As one delves deeper into Homotopy Type Theory, the sheer density of the formalism can easily obscure the underlying mathematical landscape. The theory is rigorous and expressive, but without a guiding structure, the reader risks drowning in an alphabet soup of dependent types, quantifiers, and paths.
In Zermelo-Fraenkel set theory, equality is extensional: two sets are equal if they have the same elements. In classical Type Theory, equality is intensional (opaque): two things are equal only if they share the exact same construction. HoTT mediates between these two extremes by introducing observational equality, where elements are deemed equivalent based on their behavior, formulated as paths in a space.
Unifying these concepts requires a systematic approach. When characterizing the identity type for various basic types, a recurring five-step framework emerges, even if the HoTT book does not always label it explicitly. The process involves defining a base code, a transport mechanism, and the mutually quasi-inverse functions encode and decode.
By codifying an opaque path into a visible structure (encoding) and then reconstructing a path from its parts (decoding), we eliminate the mystery of the identity type. Applying this framework systematically reveals the elegant similarities between different types. For instance, the encoding for independent pairs $A \times B$ simply maps paths using the standard $\mathbf{ap}$ function, whereas for dependent pairs ($\Sigma$-types), the second coordinate naturally swaps $\mathbf{ap}$ for $\mathbf{apd}$ (the dependent version). Recognizing this framework transforms seemingly ad-hoc proofs into predictable, structural refactorings.
While the framework unifies equality, translating concepts from other branches of mathematics into HoTT presents its own hurdles. A prime example is the concept of a pullback from Category Theory.
In Category Theory, proving that a pasted square is a pullback if its components are pullbacks is a relatively straightforward diagrammatic exercise. However, attempting a word-for-word translation of this universal property into HoTT is a descent into madness. A commutative square in HoTT is not just a property; it is an inhabitant of an identity type. Because universal properties postulate existence and uniqueness, a literal translation requires tracking 1-paths, 2-paths (equalities between equalities), and even 3-paths. The complexity quickly scales into a wall of unmanageable conditions.
The breakthrough comes from realizing that HoTT demands a different paradigm. Instead of translating the rigid, classical conditions of a universal property, we must express it as an equivalence of types. By defining the pullback as the diagram that realizes the equivalence between the type of commutative cones and the type of maps to the pullback object, the paralyzing complexity evaporates. The lesson is clear: translating universal properties faithfully is a terrible idea; expressing them as adjoint functors or type equivalences is the elegant path forward.
Despite its heavy syntactic nature, HoTT is deeply connected to geometry. The topological analogy—treating types as spaces and equalities as continuous paths—allows us to visualize purely synthetic logical statements.
When dealing with higher-order equalities, such as whiskering (concatenating a 2-path with a 1-path), graphical representation becomes indispensable. Drawing a diagram of a fibration—where paths in the base space lift to paths in the total space—can instantly clarify the strategy of a proof. It is remarkable that a theory so fundamentally rooted in formal logic and syntactic computation admits such simple and intuitive visual representations.
By translating the symbolic into the geometric, we give ourselves a map. The diagrams prevent us from getting lost in the notation, reminding us that behind every complex expression lies a structured, navigable space.
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