Timeline for Function extensionality: does it make a difference? why would one keep it out of the axioms?
Current License: CC BY-SA 3.0
33 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 1, 2021 at 13:28 | comment | added | Andrej Bauer | Sure, let $\Gamma$ be the context $m : \mathbb{N}, n : \mathbb{N}, p : \mathrm{Id}(m, n)$. Then $\Gamma \vdash p : \mathrm{Id}(m, n)$ but $\Gamma \not\vdash m \equiv n : \mathbb{N}$. In pure Martin-Löf type theory this is the best we can do (i.e., for closed term propositional equality implies judgemental equality). If we pass to some other kind of type theory, such as Observational type theory, then we will have "real" example (in OTT $\mathrm{tr}(\mathrm{add})$ and $\mathrm{add}$ are closed terms that are propositionally equal but not judgementally equal). | |
| Mar 1, 2021 at 12:12 | comment | added | Faris | But then doesn't extensional equality always imply intensional equality? Can you specify a type system, a type in it and two terms of that type that are extensionally equal but not intensionally equal? As you say $\mathrm{add}, \mathrm{tr}(\mathrm{add}):\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ in Martin-Löf type theory doesn't work since these terms are neither extensionally equal nor intensionally equal. | |
| Mar 1, 2021 at 7:07 | comment | added | Andrej Bauer | $\mathrm{tr}(\mathrm{add})$ and $\mathrm{add}$ cannot be proved to be equal in any sense, extensional or intensional. You might be confusing $\mathrm{Id}(\mathrm{tr}(\mathrm{add}), \mathrm{add})$ and $\Pi(x, y : \mathbb{N}) \, \mathrm{Id}(\mathrm{tr}(\mathrm{add})(x,y)), \mathrm{add}(x,y))$ (that's another notion of equality for functions, confusingly know as "extensional equality of functions"). | |
| Feb 28, 2021 at 10:26 | comment | added | Faris | I see. But then the sentence "The intensional one is called "judgmental" or "definitional equality" $\equiv$ and the extensional one is known as "propositional equality" $=$" in your answer is misleading (since $\mathrm{add}$ and $\mathrm{tr}(\mathrm{add})$ are not propositionally equal but are extensionally equal). | |
| Feb 17, 2021 at 13:36 | comment | added | Andrej Bauer | No it would not. How do you indent to prove $\mathrm{Id}(\mathrm{tr}(\mathrm{add}), \mathrm{add})$? | |
| Feb 17, 2021 at 13:10 | comment | added | Faris | Thank you. So then if we defined addition as a closed term $\mathrm{add}:\mathbb{N}\times \mathbb{N}\to\mathbb{N}$ and considered the transposition of arguments $\mathrm{tr}:(\mathbb{N}\times \mathbb{N}\to\mathbb{N})\to (\mathbb{N}\times \mathbb{N}\to\mathbb{N})$ the judgment $\mathrm{tr}(\mathrm{add})\equiv \mathrm{add}$ would hold? | |
| Feb 17, 2021 at 9:14 | comment | added | Andrej Bauer | That would be all types, at least in a strongly normalizing theory. Suppose $p : \mathrm{Id}_T(t, t')$. Because $p$ is closed it normalizes to $\mathrm{refl}$, therefore $t \equiv t'$. | |
| Feb 17, 2021 at 9:01 | comment | added | Faris | Thank you for your explanation. Then I wonder for which types $T$ is it true that given any two closed terms $t, t':T$ if the type $\mathrm{Id}_{T}(t, t')$ is inhabited then $t\equiv t'$? This is of course a metatheoretical property because it features judgmental equality. It seems to hold for $\mathbb{N}$ and also for any type with only finitely many judgmentally distinct closed terms. As you point out it's not true for $\mathbb{N}\to\mathbb{N}\to\mathbb{N}$. | |
| Feb 14, 2021 at 9:24 | comment | added | Andrej Bauer | @Faris: you can prove for any closed terms $e_1$ and $e_2$ that $e_1 + e_2 \equiv e_2 + e_1$, but you cannot prove the judgemental equality $x + y \equiv y + x$ where $x$ and $y$ are variables. The induction principle for the natural numbers works on types, not judgemental equalities. | |
| Feb 14, 2021 at 5:08 | comment | added | Faris | I don't understand why is addition of natural numbers not judgmentally commutative. Isn't it true that if two functions are pointwise judgmentally equal then they are judgmentally equal? Then considering addition and addition with transposed arguments as terms of $\mathbb{N}\to\mathbb{N}\to\mathbb{N}$ we can prove judgmental equality for a fixed value of the first parameter and from that conclude judgmental equality. | |
| Sep 29, 2016 at 14:27 | comment | added | Ben Millwood | Equally cute :) | |
| Sep 29, 2016 at 13:41 | comment | added | Todd Trimble | @BenMillwood Thanks for educating me here (although the application of the word, as for example in Andrej's post, seems to be wider than what was explained in the jargon file). Here's another place where '-matic' is changed to '-magic': kurims.kyoto-u.ac.jp/EMIS/journals/SLC/wpapers/s44cartier1.pdf | |
| Sep 27, 2016 at 16:23 | comment | added | Andrej Bauer | @BenMillwood: it's dangerous to introduce mathematicians to the jargon file. They'll start saying things like "I had a nasty bug. It turned out to be an Obi-Wan." | |
| Sep 27, 2016 at 16:00 | comment | added | Ben Millwood | @ToddTrimble the word has a longer history than you realise | |
| Sep 2, 2016 at 12:08 | comment | added | Todd Trimble | If "automagically" was a typo and you meant "automatically", then I think it should still not be corrected: "automagically" is a great portmanteau! | |
| Dec 30, 2015 at 9:27 | comment | added | Andrej Bauer | Possibly yes, I read it somewhere in Russell and wasn't careful about the fact that he could have picked it up from Frege. | |
| Dec 30, 2015 at 3:19 | comment | added | Bruno Bentzen | "To use Russell's example, intensionally the morning star and the evening star are clearly not the same " - Isn't it Frege's example from Über Sinn und Bedeutung (1892)? | |
| Jun 27, 2014 at 3:37 | comment | added | Toby Bartels | It is (or can be) consistent even to deny excluded middle, just not to deny any instance of it. That is, you may assert $\neg(\forall P\colon \operatorname{Prop}, P \vee \neg{P})$ but not $\exists P\colon \operatorname{Prop}, \neg(P \vee \neg{P})$. The Russian and intuitionistic schools of constructivism do this (not directly, but as a consequence of other, more interesting axioms). | |
| May 28, 2014 at 17:42 | comment | added | Jonathan Sterling | Here's a link to the relevant paper: Observational Equality, Now!. All I claimed is that an explicit setoid construction is not necessary to get proper equality for functions and quotients of hsets. It is very unlikely that the original post had in mind an extensional equality for anything higher than hsets. It will be very interesting to watch type theorists make extensionality principles for types in general compute, of course! | |
| May 28, 2014 at 5:06 | comment | added | Andrej Bauer | @JonathanSterling: yes of course it is worth referring to Observational Type Theory (OTT), maybe even with a URL? That would be helpful. I disagree that a final "solution to quotients" was found by type theorists a decade ago. In fact, I would say we only know how to handle quotients of $0$-types (hsets). | |
| May 28, 2014 at 2:34 | comment | added | Jonathan Sterling | To elaborate, if all you want is funext and quotients in ITT, you need only look back a decade to find all the tools you need to construct them without resorting to a clunky setoid construction. HoTT is awesome, but we don't need to figure out the computational content of univalence just to get extensionality principles for hsets. | |
| May 28, 2014 at 2:30 | comment | added | Jonathan Sterling | @AndrejBauer: I don't think it's accurate to say that having a computational interpretation of function extensionality is "desirable", as though we do not already have one. Indeed, the only extensionality principle that (so far) lacks a satisfying computational interpretation is univalence. Since the 90s, we have known how to integrate extensionality principles like funext into intensional type theory by internalizing the setoid construction you mention into the syntax of TT itself. Altenkirch/McBride's OTT is an example of doing this which does not lose any of the nice properties of ITT. | |
| Feb 1, 2014 at 7:16 | comment | added | Andrej Bauer | That's nothing, ask Google about HoTT models. | |
| Jan 31, 2014 at 20:31 | comment | added | Jason Rute | "HoTTest open problem" :) | |
| Jan 31, 2014 at 17:19 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 55 characters in body
|
| Jan 31, 2014 at 16:47 | comment | added | darij grinberg | Thanks -- I accepted the answer and edited the question. If you could hint me towards a setoid tutorial (for Coq), I'd be particularly indebted. | |
| Jan 31, 2014 at 16:44 | vote | accept | darij grinberg | ||
| Jan 31, 2014 at 16:43 | comment | added | Andrej Bauer | Oh. I updated my answer to make it clear that the setoid model shows that function extensionality does not add any power, in the sense that we can build a model satisfying it starting from a theory without function extensionality. Regarding "not accept" versus "deny", I suggest strongly that you do not confuse them. There are a lot of ordinary mathematicians who confuse "not accept excluded middle" with "deny excluded middle". Because the denial of excluded middle is false (constructively and otherwise), they then wrongly conclude that constructive mathematicians are crazy. | |
| Jan 31, 2014 at 16:40 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 214 characters in body
|
| Jan 31, 2014 at 16:31 | comment | added | darij grinberg | Thanks for the reply! +1 (but no accept because I'd really love to see question 2. answered, nothing personal). So funext would break some normalization/diamond properties that equalities otherwise have? Also, a quick remark: I abused "deny" to mean "leave out of the axioms". (I have yet to see an axiom whose pure negation would be of any interest.) Is "not accept" really much less confusing? If so, I'll fix the title. | |
| Jan 31, 2014 at 15:45 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 12 characters in body
|
| Jan 31, 2014 at 15:37 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 12 characters in body
|
| Jan 31, 2014 at 14:48 | history | answered | Andrej Bauer | CC BY-SA 3.0 |