Timeline for Extensionality in HoTT versus extensionality in internal language of a category
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 3, 2014 at 16:20 | comment | added | Andrej Bauer | No, $\beta$-reduction is a judgmental equality which describes what happens when we apply the eliminator (application) to a constructor ($\lambda$-abstraction). The eliminator is the proof term which corresponds to an elimination rule. | |
| Nov 3, 2014 at 15:54 | comment | added | user40276 | By an eliminator you mean $\beta$-reduction? | |
| Nov 3, 2014 at 15:43 | comment | added | Andrej Bauer | No. Types are not observations, and neither are elements of a type observations. An observation is an application of an eliminator to an element of a type, and then it is an observation about the element. At best you could say that $\mathsf{Id}$ is the internal version of $\equiv$, and that it is possible to make observations about the elements of $\mathsf{Id}$. But certainly there is no such thing as "observation about $x \equiv_A y$", at least not in the sense I am talking about. | |
| Nov 3, 2014 at 15:26 | comment | added | user40276 | $Id_A (x, y)$ is the observation that $x \equiv_A y$, so it would make sense that it's the extension of $x \equiv_A y$, this is my point. But I want to know the initial idea of Martin-Löf using his ideas of proposition and judgment. | |
| Nov 3, 2014 at 15:19 | comment | added | Andrej Bauer | I never thought of $\mathsf{Id}$ as the internal version of $\equiv$, actually, but I've heard people say that. If you are already familiar with the concept of internalization, it's probably best to think that $\mathsf{Id}$ is not the internal version of $\equiv$, at least for a start. Although, I am sure there is a way to look at it as internalization, since $\mathsf{Id}_A$ is the "the least (internal) equivalence relation on $A$". The thing to keep in mind is that in a proof-relevant setting such a relation need not be the diagonal $A \to A \times A$. | |
| Nov 3, 2014 at 15:05 | comment | added | user40276 | 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? | |
| Nov 3, 2014 at 14:48 | comment | added | Andrej Bauer | 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. | |
| Nov 3, 2014 at 14:46 | comment | added | Andrej Bauer | "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. | |
| Nov 3, 2014 at 14:42 | comment | added | Andrej Bauer | 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. | |
| Nov 3, 2014 at 13:55 | comment | added | user40276 | 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? | |
| Nov 3, 2014 at 8:57 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
deleted 8 characters in body
|
| Nov 3, 2014 at 8:47 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
deleted 8 characters in body
|
| Nov 3, 2014 at 8:41 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 317 characters in body
|
| Nov 3, 2014 at 8:34 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 573 characters in body
|
| Nov 3, 2014 at 8:25 | history | answered | Andrej Bauer | CC BY-SA 3.0 |