[[Homotopy Type Theory]] ([[HoTT]]) is a relatively new field of mathematics that combines principles from homotopy theory and type theory. It seeks to provide a foundation for mathematics and logic that is based on the idea that types can be seen as spaces and proofs as paths in these spaces. ## Some caveat before studying HoTT Before studying [[HoTT]], reading [[@cusmariuLogicKidsAll|Logic for Kids: All Aboard the Therefore Train!]] and then [[The Little Series]] can be very helpful. # Now Back to HoTT In HoTT, types are considered to be spaces with elements inhabiting them, and the relationships between these elements are described by paths. These paths can be seen as proofs of equality or equivalences between elements of a type. This perspective allows for a more geometrical understanding of logic and mathematics. One of the central ideas in HoTT is the principle of [[univalence]], which states that isomorphic types can be considered equal. This means that two types are equivalent if there exists a bijection between their elements. This principle has implications for various areas of mathematics, including category theory, algebraic topology, and higher-dimensional algebra. HoTT also provides a computational interpretation of logic through its connection to type theory. It allows for the use of dependent types, which are types that depend on values or other types. This enables precise specification and verification of computer programs. # HoTT vs. CTT [[Cubical Type Theory]] ([[CTT]]) and [[Homotopy Type Theory]] ([[HoTT]]) are closely related frameworks within the field of dependent type theory. Both share a common foundation in [[Martin-Löf type theory]] and explore the connection between logic, computation, and higher-dimensional homotopy theory. **Here's a breakdown of their connection:** **Shared Foundations:** - **Martin-Löf Type Theory:** Both CTT and HoTT build upon Martin-Löf type theory, which introduces [[dependent types]] and proofs as first-class citizens within the formal system. This allows for more expressive and powerful type-theoretic reasoning. - **Univalence Axiom:** Both frameworks incorporate the Univalence Axiom, which states that equivalent types are homotopy equivalent. This axiom establishes a deep connection between logic and homotopy theory, allowing for proofs to be interpreted as paths in a space. **Distinctive Features:** - **Cubical Sets:** CTT utilizes cubical sets as its underlying model, which are higher-dimensional generalizations of sets with additional structure like faces and degeneracies. This structure gives rise to a richer notion of homotopy equivalence and allows for more efficient proofs in certain contexts. - **Higher Inductive Types:** HoTT introduces a broader range of higher inductive types (HITs), such as circles and spheres, which directly reflect higher-dimensional homotopy types. These HITs provide a richer language for expressing and reasoning about homotopy-theoretic concepts. **Complementary Roles:** - **Computational focus:** CTT's emphasis on cubical sets makes it computationally attractive, leading to the development of efficient type checking and proof normalization algorithms. - **Conceptual clarity:** HoTT's extensive use of HITs provides a more conceptually clear and intuitive framework for understanding homotopy theory and its connections to logic and computation. **Benefits of their relationship:** - **Mutual enrichment:** Both frameworks benefit from insights and developments within the other. CTT's computational efficiency complements HoTT's conceptual clarity, while HoTT's expressive power inspires new applications and theoretical developments in CTT. - **Diversification and exploration:** The existence of two distinct frameworks with overlapping foundations allows for exploration and development of different approaches to type theory and homotopy theory. This diversity encourages innovation and fosters a richer understanding of these fields. [[Cubical Type Theory]] and [[Homotopy Type Theory]] represent **two sides of the same coin** (also see [[Three Dimensional Logic Model Designs]]), each offering unique advantages and contributing significantly to the advancement of type theory and its applications in mathematics, computer science, and other fields. # Conclusion Overall, Homotopy Type Theory aims to bridge the gap between logic, mathematics, and computer science by providing a unified framework for reasoning about both abstract mathematical structures and computational processes. It has applications in various fields such as formal verification, proof assistants, automated theorem proving, and theoretical computer science. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Homotopy Type Theory") or contains(subject, "HoTT") or contains(title, "Homotopy Type Theory") or contains(title, "HoTT") ```