[[Intensional Type Theory]] is a formal system that combines elements of type theory and logic. It was developed by [[Per Martin-Löf]] as an extension of his earlier work on intuitionistic type theory. In Intensional Type Theory, types are seen as collections of objects that share certain properties or characteristics. These types are used to classify the terms in the system, which represent objects or values. The idea is that the type of a term determines its behavior and how it can be used in a proof or computation. One key feature of Intensional Type Theory is its **treatment** of [[equivalence|equality]]. In this system, equality is considered to be Intensional rather than extensional. This means that two terms are considered equal if they have the same intension or meaning, rather than if they have the same extension or set of instances. Another important aspect of Intensional Type Theory is its support for dependent types. Dependent types allow the type of a term to depend on the value of another term, enabling more precise and expressive specifications. # Intensional and Extensional Type Theory [[Intensional Type Theory]] ([[ITT]]) and [[Extensional Type Theory]] ([[ETT]]) are two different approaches to the foundations of mathematics and logic. While both theories are based on the notion of types, they differ in how they handle equality and extensionality. 1. Equality: - ITT: In ITT, equality is defined as an Intensional notion. It means that two objects are equal if they have the same properties or can be substituted for each other in all contexts without changing the truth of statements. For example, in ITT, two functions are considered equal if they produce the same output for every input. - ETT: In ETT, equality is defined as an extensional notion. It means that two objects are equal if they behave indistinguishably or produce the same results under all circumstances. In ETT, functions are considered equal if they produce the same outputs for all possible inputs. 2. Extensionality: - ITT: ITT does not assume extensionality as a fundamental principle. This means that in general, two functions with different definitions but producing the same output for all inputs are not considered equal. - ETT: ETT assumes extensionality as a fundamental principle. This means that two functions with different definitions but producing the same output for all inputs are considered equal. 3. Computational interpretation: - ITT: ITT has a strong computational interpretation where types can be seen as sets of values and terms as programs that compute those values. - ETT: ETT also has a computational interpretation but places less emphasis on computation and more on logical reasoning. 4. Proof theory: - ITT: ITT is often associated with constructive or intuitionistic logic, where proofs provide evidence for the truth of statements. - ETT: ETT is often associated with classical logic, where proofs establish truth without providing explicit evidence. In summary, while both Intensional Type Theory and Extensional Type Theory are based on the notion of types, they differ in their treatment of equality and extensionality. ITT defines equality Intensionally based on properties and substitution, while ETT defines equality extensionally based on behaviors and indistinguishability. # Conclusion Intensional Type Theory has been influential in various areas, including [[programming language design]] and [[formal verification]]. It provides a foundation for constructing formal proofs and reasoning about properties of programs and systems. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Intensional") ```