Cubical Type Theory (CTT) is an extension of [[Martin-Löf Type Theory]] (MLTT) that introduces a new dimension into the logic. It was developed by [[Thierry Coquand]] and [[Simon Huber]] in 2013. CTT aims to provide a computational foundation for homotopy type theory, which connects abstract algebraic topology with constructive mathematics. In CTT, types are interpreted as spaces and terms as points in those spaces. The new dimension, called [[cubical dimension]], allows for reasoning about paths and higher-dimensional structures in a type. This makes it possible to express concepts from homotopy theory directly within the type theory. CTT introduces several new constructs to support reasoning about paths and higher-dimensional structures. For example, it includes a new type called the interval type, denoted as I, which represents the closed interval [0,1]. Paths between points can be defined by functions from I to a type. Additionally, CTT introduces new rules for path formation and transport along paths. These rules allow for reasoning about equality between terms along paths and higher-dimensional structures like squares or cubes. CTT has several applications in computer science and mathematics. **CTT provides a foundation for [[Homotopy Type Theory]]**, which has connections to fields such as algebraic topology and [[category theory]]. It also has practical applications in programming languages with dependent types, allowing for more expressive programming languages that can reason about equality between terms. ![[Homotopy Type Theory#HoTT vs. CTT]] Also see: [[Simplex#Simplex in Cubical Type Theory]] ![[Simplex#Simplex in Cubical Type Theory]] # Conclusion Overall, [[Cubical Type Theory]] extends [[Martin-Löf Type Theory]] by introducing a [[cubical dimension]] that enables reasoning about paths and higher-dimensional structures within the type theory framework. It provides a computational foundation for homotopy type theory and has applications in various domains of computer science and mathematics. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Cubical Type Theory") or contains(subject, "cubical type theory") or contains(subject, "Topology") or contains(subject, "Cubical") ```