Timeline for Practical example in using (homotopy) type theory
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 18, 2019 at 19:23 | comment | added | Mike Shulman | FWIW, choice is irrelevant for most purposes when dealing with finiteness; excluded middle is enough to make most definitions of "finite" coincide and behave the way a classical mathematician expects. The only exception I'm aware of is the notion of "Dedekind-finite set" which requires a small amount of choice (even less than countable choice) to prove equivalent to all the other notions of finiteness; but that definition is I think very rarely used in practice. And, as Valery has stressed, this is an issue of constructiveness that is completely orthogonal to HoTT vs ZFC. | |
| Jul 18, 2019 at 18:22 | history | edited | Valery Isaev | CC BY-SA 4.0 |
edited body
|
| Jul 18, 2019 at 18:15 | comment | added | Noah Snyder | Are these things easy in classical foundations? You still need to define what a finite set is, and you still need to prove finite choice, subsets of finite sets are finite, and quotients of finite sets are finite. Working constructively makes things harder, but if you throw in excluded-middle and choice, then it doesn't seem to me that the difficulty is much different in classical foundations or in type theoretic foundations (none of this is about homotopy types). Either way you have to think a bit about why finite sets work the way you think they do. | |
| Jul 18, 2019 at 16:45 | comment | added | François G. Dorais | @AndreaFerretti No, even sets are a problem. The issue with choice is decidable equality, for example. | |
| Jul 18, 2019 at 16:43 | comment | added | Valery Isaev | No, these are all definitions of finite sets. It is even less clear how to define finite types. Let me note once again, this problem is the problem of constructive mathematics. It will be the same in other constructive theories such as CZF and IZF. | |
| Jul 18, 2019 at 16:38 | comment | added | Andrea Ferretti | @FrançoisG.Dorais Do these notions agree at least for sets or are there different notions of finite set in HTT (without choice and excluded middle?) | |
| Jul 18, 2019 at 16:37 | comment | added | Andrea Ferretti | Ok, things are getting weirder than I would expect :-D It is a strange foundation indeed that in which there are several, different, notions of finite... | |
| Jul 18, 2019 at 16:35 | comment | added | François G. Dorais | @AndreaFerretti Choice is not the issue, you need to correctly define "finite". There are several different ways to do this in HTT, but they all coincide assuming excluded middle and choice. Once you investigate what "finite" means, you will notice that "finite choice", "subtypes of finite types are finite", "quotients of finite types are finite" are (independently of each other) provable in HTT for some but not all variations of "finite". For Lagrange's Theorem, you need all three of these to work simultaneously, or you need to restrict what you mean by "subgroup". | |
| Jul 18, 2019 at 16:20 | comment | added | Andrea Ferretti | Does 2. mean that the "proof" sketched above would not be valid in HTT, but would be valid in HTT+excluded middle+choice? In ZFC we don't need finite choice, but in this constructive world I am not sure. Is Lagrange theorem even true in HTT? | |
| Jul 18, 2019 at 15:40 | history | answered | Valery Isaev | CC BY-SA 4.0 |