Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
What the technical part of the discussion in the entry really refers to is the fact that the term “2+2” and the term “5” are equal as proofs of the proposition that “ is inhabited”.
The text that is offered around this fact I find misleading and counterproductive. I vote for this entry being deleted.
The fact that sets (i.e., homotopy 0-types) can be localized to get homotopy (-1)-types (i.e., truth values) is nice, but clearly does not belong in a separate article, and Section 3 (Philosophical consequences) is stretching things too far.
Are the natural numbers actuslly the natural numbers if every type is (-1)-truncated? (similarly goes for the circle type in the presence of UIP)
I agree that this article is not a productive contribution to the nLab, and further, the title was the subject of a wide-ranging debate spanning everything from maths education to hot-button political topics a couple of years ago.
If one wants a technical discussion as at the page, then I think it might fit on a different page that is about the overarching concept that is being interrogated (eg weak systems of arithmetic, or homotopy (-1)-types etc).
1 to 6 of 6