[Type theory](https://www.wikiwand.com/en/Type_theory) or [[intuitionistic type theory]] is a formal system used in computer science, mathematics, and philosophy to study the properties of mathematical objects and their relationships. It provides a foundation for constructing and reasoning about programs, proving theorems, and understanding the structure of mathematical concepts. It is particularly useful in [[Namespace Management]]. In type theory, every expression has a type associated with it, which defines the set of values that expression can take. Types can be simple (e.g., numbers or booleans) or complex (e.g., functions or sets). The type system ensures that expressions are used in a consistent manner, preventing errors such as adding a number to a string. One key aspect of type theory is the concept of [[dependent types]]. Dependent types allow types to depend on values, enabling more precise specifications and more expressive programming languages. This allows for advanced features like dependent function types and dependent pattern matching. Type theory also includes notions such as type inference, which automatically deduces the types of expressions based on their context, and parametric polymorphism, which allows functions to be applied to arguments of different types. # What are the main branches of Type Theory The main branches of Type Theory are: 1. [[Martin-Löf Type Theory]] ([[MLTT]]): Developed by Per Martin-Löf, MLTT is one of the most widely studied and used branches of Type Theory. It is a constructive type theory that provides a foundation for both mathematics and computer science. 2. [[Homotopy Type Theory]] ([[HoTT]]): Homotopy Type Theory combines concepts from homotopy theory and type theory. It explores the relationship between spaces and types, with the aim of providing a foundation for mathematics based on higher-dimensional structures. 3. [[Extensional Type Theory]] ([[ETT]]): Extensional Type Theory focuses on equality between types or terms, allowing for more flexible reasoning about equality compared to intensional type theories. 4. [[Intensional Type Theory]] ([[ITT]]): Intensional Type Theory emphasizes computational aspects and proofs-as-programs interpretation, where types are seen as sets or collections of values. 5. [[Dependent type theory]]: Dependent Type Theory extends traditional type systems by allowing types to depend on values, enabling more expressive and precise specifications of programs or mathematical structures. 6. [[Categorical Type Theory]]: Categorical Type Theory bridges the gap between [[category theory]] and type theory by using category-theoretic concepts to study the structure and properties of types. 1. [[Constructive Set Theory]]: Constructive Set Theory is an alternative to classical set theory that is based on constructive logic principles, where sets are defined in terms of their elements and the operations that can be performed on them. 2. [[Naïve Type Theory]] ([[NTT]]) is a foundational theory in the field of mathematics and computer science. It is based on the concept of types, which classify mathematical objects and expressions. NTT treats types as first-class citizens, meaning that they can be manipulated and used as objects themselves. 3. [[@YonedaEmbeddingExpresses2023|The Yoneda Embedding Expresses Whether, What, How, Why]]: The [[WH questions]] can be expressed in Category Theory, and provides a natural language interpretation of [[Type Theory]]. These branches of Type Theory often overlap and influence each other, leading to further developments in the field. # Conclusion Overall, type theory provides a rigorous framework for specifying and verifying the behavior of programs and mathematical proofs. It has influenced the development of programming languages like [[Haskell]], [[Coq]], and [[Agda]], as well as various branches of mathematics and philosophy. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Type Theory") or contains(title, "Type Theory") or contains(subject, "type theory") or contains(title, "type theory") ```