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.

  • $\begingroup$ Do you have an example of a "simple" extensional type theory? To my mind, Martin-Löf is pretty simple, although maybe I'm just ignoring all the complexity. $\endgroup$ Jul 5, 2022 at 21:13
  • $\begingroup$ @PatrickStevens ... I'm okay with a toy system that has no practical use. I'm just trying to get a sense for how to look at a type system and assess whether it is intensional or not ... and understand why we need or would want intensionality if what we're trying to do is build a groupoid out of a type system. $\endgroup$ Jul 5, 2022 at 21:21
  • $\begingroup$ This answers some of your question en.wikipedia.org/wiki/… $\endgroup$ Jul 5, 2022 at 22:55

1 Answer 1


$\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

  • In its intensional form, it has sufficient computational content to function as a programming language.
  • At the same time, it has identity types whose presence shows that one is really dealing with a form of homotopy type theory.

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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .