What is an intensional type theory and what is a simple example of one?
I'm interested in understanding the sentence below in the prehistory section of the Wikipedia article on Homotopy Type Theory.
At one time the idea that types in intensional type theory with their identity types could be regarded as groupoids was mathematical folklore.
I'm reading this sentence as every intensional type system with identity types is associated with a groupoid.
This, to my naive understanding, makes more sense if we restrict attention to cases where equalities are always types and hence always have proof objects witnessing their truth. In this way, the objects of the groupoid are types and the morphisms of the groupoid are proofs of $A = B$.
A groupoid, definitionally, is very simple. It is a category where every arrow is invertible.
Intensional type theories are harder to get a handle on.
The nCatlab definition is given below.
Intensional type theory is the flavor of type theory in which identity types are not necessarily propositions (that is, (-1)-truncated). Martin-Löf‘s original definition of identity types, and the equivalent formulation as an inductive type, are by default intensional; one has to impose extra axioms or rules in order to get extensional type theory (in which identity types are propositions).
In particular, homotopy type theory is intensional, because identity types represent path objects.
I'm not sure what to make of these two examples.
Both of the examples that they give are large, complicated systems. Additionally,
Martin-Löf type theory, as far as I know, has both equality judgments and equality types.
Best Answer
$\def\opn{\operatorname}$ In Martin-Löf's dependent type theory, a notion of equality is said to be "intensional" if it distinguishes objects based on their particular definitions, and "extensional" if it does not distinguish objects that have the same observable behaviour.
Therefore, intensional type theory is so named because its judgmental equality $x \equiv y$ is an intensional equality : it says essentially that $x$ and $y$ have the same definition. By contrast, the propositional equality $x =_A y$ is more of an extensional equality. Hence, extensional type theory is so named because it does not admit any purely intensional equality by assuming a reflection rule that forces the judgmental equality to coincide with the more extensional identity type $$\frac{\Gamma \vdash p : \opn{Id}_A(x, y)}{\Gamma \vdash x \equiv y}$$
Regarding Martin-Löf's constructive type theory, we can see that
It appears that homotopy type theory has been revealed to be a practical tool when working with $\infty$-groupoids, because we do not need to define it (describing such structure in set theory is notoriously known to be a difficult task). Instead, we exploit the fact that every type in type theory is an $\infty$-groupoid, with the structure of morphisms, $2$-morphism, $3$-morphisms, … given by the identity type propositional (therefore extensional) equality.