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?

  • $\begingroup$ I am not sure it makes sense to speak of the "extension of judgmental equality" (please do not call it "definitional") because judgmental equality is not a type or an element of a type, or anything like that. It is a judgment. $\endgroup$ – Andrej Bauer Nov 3 '14 at 16:19
  • $\begingroup$ @AndrejBauer the judgmental equality is definitional (actually computational). Furthermore it's an element of the deductive system, so it's part of the metalanguage, so it makes sense to talk about extensions. Maybe this question is quite subjective since "extension" is a philosophical concept… $\endgroup$ – user40276 Nov 3 '14 at 19:56
  • $\begingroup$ But I agree that definitional is just a characteristic of the judgmental equality, so I will change it. $\endgroup$ – user40276 Nov 3 '14 at 21:29
  • 1
    $\begingroup$ The extension of a predicate $P : A \to \mathsf{Type}$ is the type $\sum_{x : A} P(x)$. $\endgroup$ – Andrej Bauer Nov 3 '14 at 21:43
  • $\begingroup$ @AndrejBauer Are you assuming "proposition as types" or you are restricting the values of $P$ to h-level 1 types? Furthermore in this case seeing $Id_A(x, y)$ and $x \equiv_A y$ as a type, their extensions would be the dependent sum, does this match with the definition of (definitionally) extensional type theory? $\endgroup$ – user40276 Nov 4 '14 at 8:54

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.

  • $\begingroup$ Thanks for the long answer. So, is it right to say that $Id_A (x, y)$ is the extension of $x \equiv y$? In this case, the extension are the proofs and not the values attained (of a predicate or function). And in the end, internal language of a category (as treated in categorical logic) is totally different from HoTT (even in the case of internalization of predicates). Am I right? $\endgroup$ – user40276 Nov 3 '14 at 13:55
  • $\begingroup$ It is wrong to say that $\mathsf{Id}_A(x,y)$ is the extension of $x \equiv_A y$. The two equalities play different roles. Judgmental equality is substitutional: it tells us when we may safely substitute one expression for another. Propositional equality is observational: it tells us when two things are observationally indistinguishable. Extension as as a set (as in "the extension of a predicate") only makes sense in set theory. In general, the correct generalization of extension is observational equivalence. $\endgroup$ – Andrej Bauer Nov 3 '14 at 14:42
  • $\begingroup$ "Totally different" is a matter of opinion. The internal language of a category in the classical sense (using the subobject fibration) is a special case of type theory in which the reflection rule is valid, and so there is only one notion of equality. But note that categorical logic also treats models of intensional type theory, except those are not expressed as subobject fibrations. $\endgroup$ – Andrej Bauer Nov 3 '14 at 14:46
  • $\begingroup$ Furthermore, "the values attained" are never the extension of anything. At best you need to pair up arguments with the corresponding values and look at the set of such pairs, or graphs of morphisms in a categorical setting. $\endgroup$ – Andrej Bauer Nov 3 '14 at 14:48
  • $\begingroup$ Ok, but as I understand, $Id_A(x, y)$ is a way to internalize a judgment $x\equiv_A y$ as a proposition (where judgment and proposition means the same as here docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf ). And in the case of the "standard" internalization (as it's here ncatlab.org/nlab/show/internal+logic) any predicate is internalized as it extension (in the sense of the collection of terms that satisfies the predicate), so considering judgmental equality as a predicate in the metalanguage we could do the same. So internalize is not the same as consider the extension? $\endgroup$ – user40276 Nov 3 '14 at 15:05

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.

  • $\begingroup$ Thanks for the answer. But do you have idea (or just a guess!) of what would be the extension of a predicate (in the case above , it's the equality seen as a predicate) in intensional type theory? It just seems that an extension is what internalize metamathematics (maybe in the sense of Gödel), so in this case the extension of $x \equiv y$ seems to be $Id_A (x, y)$ (the proofs)… And, if this is the case, it's incompatible with predicates in the internal language of categories (as it's here for instance ncatlab.org/nlab/show/internal+logic ). $\endgroup$ – user40276 Nov 3 '14 at 8:04
  • $\begingroup$ I think you're not using the phrase "extension of a predicate" correctly. To me that phrase makes sense if by "predicate" you mean a textual description of a property, in which case its "extension" is the collection of things that satisfy it, i.e. "extension" is the map from syntax to semantics. For instance, in set theory the extension of $x>2$ would be the set $\{x | x>2\}$; the former is syntactic (hence lives in the metatheory) and the latter is an object of the theory itself $\endgroup$ – Mike Shulman Nov 3 '14 at 21:49
  • $\begingroup$ ... But a "predicate" in the sense of a map $P:A\to \mathsf{Type}$ in type theory is already a object of the theory, on the same level as $\{x|x>2\}$ in set theory. So the only sense in which it has an "extension" is that it is its own extension. $\endgroup$ – Mike Shulman Nov 3 '14 at 21:50
  • $\begingroup$ On the other hand, the judgmental equality $x\equiv y$ is syntactic, so we could speak about its "extension" as an object inside the theory. However, in ordinary HoTT (such as the theory used in the book) such an extension does not exist: there is no way to internalize the judgmental equality. Although Voevodsky has proposed a version of type theory that does internalize it as a "strict equality type", which is different from the ordinary propositional/path equality used most of the time in HoTT. $\endgroup$ – Mike Shulman Nov 3 '14 at 21:53
  • 1
    $\begingroup$ @RodrigoFreire, if this is a question about philosophy, then I can't answer it. I thought it was a question about mathematics. $\endgroup$ – Mike Shulman Nov 4 '14 at 1:25

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

  • 6
    $\begingroup$ You might consider editing this post to be a bit more diplomatic? $\endgroup$ – Steven Gubkin Nov 2 '14 at 19:13
  • $\begingroup$ My post was written exactly to be diplomatic, and tutorial, with a view to encouraging the questioner to pursue the study of this topic. Unfortunately, the same cannot be said of most of the responses to naive questions from students that appear on this site: similarly phrased questions on slightly different topics are peremptorily closed. $\endgroup$ – Paul Taylor Nov 2 '14 at 20:35
  • 6
    $\begingroup$ I think the first sentence of your post is not very helpful. Of course, that is just an opinion. I do not think I will comment further. $\endgroup$ – Steven Gubkin Nov 2 '14 at 20:48
  • 4
    $\begingroup$ Thanks for the answer, but I already knew everything you have said. My point is different (and I have a background in category theory), I know what $x=_A y$ means (the proofs or evidences of the equality, i.e., an internalization of a judgment). I want to know what is the extension of a predicate in HoTT. "Extension" is a concept of mathematical philosophy and in the case of classical logic (I don't know the intuitionistic case, maybe this would be the answer the my question) it's considered to be the collection of elements (terms in the context of type theory) that satisfies the predicate. $\endgroup$ – user40276 Nov 3 '14 at 7:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.