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.
I’m having trouble parsing even the first definition. Why is an object isomorphic to a (disjoint?) union of objects in the image?
I think somebody took the definition in the HoTT book and tried to translate it into set theory.
To parse this, add the missing parenthesis: What must be meat is not
but
so that under 0-truncation this gives the usual (“merely”) existence statement:
.
I hope somebody finds the energy to polish-up this entry.
I’d suggest to also either define or else replace the notation \biguplus
: The common usage of this notation is for disjoint union in set-theoretic contexts, where the crucial distinction which this entry is (or ought to be) making isn’t visible.
Fixed some notation, clarified some phrasing. Also removed several false statements:
Anonymous, please back off on these questionable rapid-fire edits. I don’t have the time to check everything you’re writing, and a lot of it is misleading, confusing, or wrong. I very much appreciate your enthusiasm for bringing HoTT into the mainstream of the nLab, but I think a better way forwards right now would be to propose particular changes on the nForum first, and only go ahead with an edit if there is general agreement. If the current situation continues, I may have to suggest some IP blocking.
1 to 8 of 8