Reflections on a Journey Through HoTT

by Leandro Caniglia

Articles

Culture Shock: First Impressions of the HoTT Book
The Mechanics of Thought - Proofs as Objects and the Limits of Human Parsing
The Architecture of Types - Judgments, Opacity, and Paths
The Geometry of Proof: Frameworks, Pullbacks, and Visualizing Complexity
Constructivism, Choice, and the Ethics of Decision
Writing as Self-Debugging - The Syntax of Thought
The Physics of Types - Magnitudes, Semantics, and Structure
The Role of Conceptual Thinking
Mechanical Verification and Hidden Dependencies: The Case of UA and FE
More Than an Allegory: The Working Logic of HoTT
A Final Reflection on Tags and Dependency Trees
What Does Induction Mean?
Beyond Simple Induction. W-Types and the Sum-Product Analogy
A Categorical Shift. Why Path Induction Makes Sense
The Literature of Symbols. Beauty and Type Theory

Welcome to HoTT Reflections

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