[[Extensional Type Theory]]([[ETT]]) is a branch of type theory that focuses on the extensional equality of types and terms. It is an alternative to [[intensional type theory]], which emphasizes intensional equality. In extensional type theory, two terms are considered equal if they have the same extension, meaning they produce the same outputs for all inputs. This notion of equality is often referred to as "extensional equality" or "observational equality." It disregards any internal structure or computational behavior of terms and focuses solely on their observable properties. One important consequence of extensional type theory is that it allows for a more flexible notion of equality between functions. In intensional type theory, two functions are considered equal if they produce the same outputs for all inputs, but their internal computations may differ. In contrast, in extensional type theory, two functions are considered equal if they produce the same outputs for all inputs and have the same computational behavior. Extensional type theory also has implications for dependent types. Dependent types allow types to depend on values, enabling more expressive and precise specifications. In extensional type theory, dependent types can be defined using extensional equality to ensure that dependent types capture the desired properties. # Intentional vs. Extentional ![[Intensional Type Theory#Intensional and Extensional Type Theory#]] # Conclusion Overall, extensional type theory provides a different perspective on equality and computation compared to intensional type theory. It emphasizes the observable behavior of terms rather than their internal structure or computation steps. This can lead to different approaches and results in various areas such as programming languages, formal verification, and proof assistants. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Extensional") ```