Extensionality in HoTT versus extensionality in internal language of a category

Question

What's the extension of judgmental identity in HoTT (homotopy type theory)?

The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the judgmental (intensional) equality coincides with the propositional equality, i.e, $$ \frac{p:Id_A(x,y)}{x\equiv y} $$ For the name "extensional" makes sense, the judgmental equality must be determined by the extension of the terms.

So what's the extension of $x \equiv y$? By the definition, it just seems that the extension are the proofs (hence $Id_A (x, y)$ is the extension of $x \equiv_A y$) and, in this case, it would not match with the extension of the relational symbol "equality" used in the internal language of categories where a relational symbol (or predicate) $\varphi$ would be a subobject of a type $A$ $$[\varphi] \hookrightarrow A$$ composed by the collection (not set, there's no set theory here) of terms such that the predicate is true $\{x : A; \varphi(x) \ \text{true} \}$ .

So, more generally, what's the extension of a predicate in Martin-Löf type theory?

Answer 1

The extension is the observable behavior, where "observation" means roughly "application of an eliminator". For a predicate $p$ we may observe whether it is true for a given argument, so by collecting those arguments at which $p$ holds we observe all there is to observe. More generally, a function is "observed" by application to an argument (as opposed to examination of its "source code" or measurement of time needed to compute, etc.), which leads to the rule of function extensionality $$\frac{x : A \vdash f(x) =_B g(x)}{f =_{A \to B} g}.$$ A simpler extensionality rule is that for cartesian products: $$\frac{\pi_1(u) =_A \pi_1(v) \qquad \pi_2(u) = \pi_2(v)}{u =_{A \times B} v} \tag{1} $$ It says that two pairs are equal if they behave in the same way when we observe them by projecting their components.

In set theory we observe a set by testing which elements it has, and so the extensionality axiom of set theory says that two sets are equal if they have the same elements. And since in set theory there are only sets, this gives set theory as much extensionality as it could have.

In the internal language of a category, say a topos, we get extensionality from universal properties, more precisely from the uniqueness requirements. For instance, (1) is validated by the fact that there is at most one morphism $C \to A \times B$ whose composition with $\pi_1$ and $\pi_2$ are prescribed maps $C \to A$ and $C \to B$. Furthermore, because in a typical internal language we interpret (judgmental) equality on $A$ as the diagonal $A \to A \times A$, which is the least equivalence relation on $A$, there is no room for another kind of equality -- the reflection principle is automatic, and so the distinction between judgmental and propostional equality does not arise.

In contrast, the intension tells us how an object is built or how it works. Thus, functions $x \mapsto x + 3$ and $x \mapsto 2 + (x + 1)$ have the same behavior, but are not intensionally equal because they compute in different ways. A typical intensional rule of equality says that two objects are equal if they are built the same way. For pairs such a rule would be $$\frac{a \equiv_A a' \qquad b \equiv_B b'}{(a,b) \equiv_{A \times B} (a',b')}.$$ Intensional equality of functions says that two functions are equal if they have the same "bodies of definition" (officially this goes under the name $\xi$-rule): $$\frac{x : A \vdash e \equiv_B e'}{(\lambda x : A \,.\, e) \equiv_{A \to B} (\lambda x : A \,.\, e')}.$$ Another kind of intensional equality explains how eliminators compute, for instance $$\pi_1(a,b) \equiv_A a$$ says that the first projection computes $a$ when applied to a pair $(a,b)$. Similarly, the $\beta$-rule for functions, $$(\lambda x : A \,.\, e_1) e_2 \equiv_B e_1[e_2/x],$$ explains how $\lambda$-abstractions compute their results, so it is again an intensional rule.

We shall therefore call a notion of equaity extensional if it makes objects equal when they have equal observations. We shall call an equality intensional if it makes objects equal when they are constructed the same way from equal parts, or if it tells us how to compute. We shall call a type theory extensional or intensional according to whether its judgmental equality is extensional or intensional (this is a source of confusion, as many people think that extensional type theory is so called because it has extensionality rules for propositional equality, see Mike Shulman's answer).

For the purposes of mathematics it is good to have extensional equality, but less so for the purposes of computer science, where we generally care how things are computed and not just what the results are. As far as type theory is concerned, we have a choice. We could declare judgmental equality to be extensional, for instance $$\frac{\pi_1(u) \equiv_A \pi_1(v) \qquad \pi_2(u) \equiv_B \pi_2(v)}{u \equiv_{A \times B} v}$$ looks reasonable. Indeed, Agda and (recent) Coq have such a rule. But things get complicated if we take this too far. The reflection rule which you stated makes judgmental equality undecidable, which does not appeal to the typical type theorist. If we make judgmental equality of functions extensional, things get at least very complicated.

It is less unreasonable to make the propositional equality extensional. This is what homotopy type theory does. It goes farther than any other kind of type theory by making the propostional equality of a universe extensional, although at the moment I cannot think of a good explanation of the Univalence axiom which starts from "what is an observation on an element of a universe".

In summary, while we have a choice to make either kind of equality extensional, it makes more sense to make propositional equality extensional and keep judgmental equality intensional.

Answer 2

In this context, an equality is said to be "extensional" if it depends on the behavior of the objects in question, and "intensional" if it depends only on their definition. I'm not entirely sure of the origin of this usage; perhaps it is a generalization from the notion of "extensionality" for predicates, where extensional equality (in the above sense) corresponds to equality of their "extensions".

So the propositional equality is extensional, because we can prove that two things are propositionally equal using their properties and behavior, whereas the judgmental equality $\equiv$ is, or at least might be, intensional, because it depends only on unfolding their definitions (broadly interpreted to include $\beta$-reduction, etc.). This is not the case in extensional type theory, where the reflection rule forces judgmental equality to also be extensional. Thus, extensional type theory is so-called because it lacks an intensional equality; all of its equalities are extensional.

Answer 3

No, sorry, but you haven't got the point of HoTT.

$x \equiv y$ means "$x$ is the same as $y$", so they are terms such that one can be transformed into the other by "rewrite rules" such as expanding or invoking the meaning of a definition, changing the names of bound variables, $\beta$-reduction, etc.

Certainly there are types systems that have rules of the kind that you propose, but the idea of HoTT is quite different from those. The clue is in the name: homotopy type theory (or indeed homotopy type theory).

I suspect that you have a pure maths background rather than one in computer science (or category theory). In that case you should think of $Id(x,y)$, not as equality, but as the fundamental group. the space of paths from $x$ to $y$.

When there is a path from $x$ to $y$, it does not mean that $x$ and $y$ are the same.

Moreover, when $p$ and $q$ are paths from $x$ to $y$, $p$ and $q$ don't have to be the same, or even homotopic.

Even when $p$ and $q$ are homotopic, so there is some $u:Id(p,q)$, there may be another $v:Id(p,q)$ that is not the same as (or homotopic to) $u$. And so on.

The expression $x\equiv y$ is not a type and does not have an extension.

The type $x=y$, written $Id(x,y)$, is that of the paths between $x$ and $y$, or of the proofs that $x$ and $y$ are equivalent, or of the equivalences between $x$ and $y$.