Timeline for Extensionality in HoTT versus extensionality in internal language of a category
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 4, 2014 at 8:29 | comment | added | Rodrigo Freire | I understand Mike Shulman, and I am not saying that your answer is not fine. I think the question is about logic, and not a purely mathematical question. My point is: logic deals (mathematically) with stuff like predicates, propositions, extensions, existence, truth, etc, which is a philosophical stuff, and I think this question touches this component of logic. | |
| Nov 4, 2014 at 1:25 | comment | added | Mike Shulman | @RodrigoFreire, if this is a question about philosophy, then I can't answer it. I thought it was a question about mathematics. | |
| Nov 3, 2014 at 23:55 | comment | added | Rodrigo Freire | In a classical and realist framework, in standard analytic philosophy, predicates, properties and propositions are not syntactic or linguistic objects. In this setting, an entity (which can be a predicate, a set, a proposition, etc) is called extensional if its identity is given by its extension. Of course, this is completely different in an intuitionistic (and idealist?) framework. | |
| Nov 3, 2014 at 21:53 | comment | added | Mike Shulman | 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. | |
| Nov 3, 2014 at 21:50 | comment | added | Mike Shulman | ... 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. | |
| Nov 3, 2014 at 21:49 | comment | added | Mike Shulman | 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 | |
| Nov 3, 2014 at 8:04 | comment | added | user40276 | 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 ). | |
| Nov 2, 2014 at 20:48 | history | answered | Mike Shulman | CC BY-SA 3.0 |