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.
The category of prosets is a coreflective subcategory of the category of topological spaces. I edited in this observation at specialization order, and am removing a query box:
+–{.query} There's an adjunction here; I should think about which way it goes and whether it's a reflection or something. —Toby Mike: If it exists, it’s either a reflection or a coreflection, since the functor is fully faithful. =–
Thanks!
adding link to specialization topology
I’d like to inquire: what is the point of this rendering into the language of dependent type theory? (This is one of many such edits I’ve seen.)
The way it appears to me, it looks analogous to a student exercise of taking simple sentences in English and translating them into Dutch. It might be a worthwhile exercise for the student of Dutch. I, even though I don’t speak Dutch, can easily tell what the Dutch sentences mean and how they correlate with the English ones, because they look rather similar, but I don’t see how it serves anyone in any real sense, except possibly other students of Dutch (or people fluent in Dutch).
A ruder take is that it looks pretentious, dressing up prosaic mathematics in hypermodern language, and overall that’s probably not a good thing, unless there’s some compelling reason for it that eludes me.
I’m not sure if this is the situation with the dependent type theory stuff on this page, but last year there were anonymous posters mass posting material from the HoTT wiki over to the nLab wiki, so among other things the nLab ended up with various pages with both a logic-over-set-theory definition and a type theory definition. (cf revision 40 of filter on June 9, 2022, and the corresponding edit on the HoTT wiki)
Thanks for the information, Madeleine. Naturally, I’d want to know: why? Is the HOTT wiki deprecated?
(My offhand guess is that not much thought went into how the transplantation would be enacted, though.)
With regard to the current page, maybe some material could be shuffled around. The type-theoretic construction of specialization, and the demonstration of Theorem 3.1: all that would go under a separate section. Since that is somewhat for specialists, if it were up to me, I’d place it more toward the end.
Naturally, I’d want to know: why? Is the HOTT wiki deprecated?
There is a message on the home page of the HoTT wiki saying that it is depreciated.
With regard to the current page, maybe some material could be shuffled around. The type-theoretic construction of specialization, and the demonstration of Theorem 3.1: all that would go under a separate section. Since that is somewhat for specialists, if it were up to me, I’d place it more toward the end.
Personally I would try to find a proof of Theorem 3.1 which does not rely on dependent type theory, since it seems to be a fairly well known theorem for topological spaces - the theorem is mentioned as fact elsewhere in the nLab such as in separation axiom. But otherwise I agree, the specifically type theoretic material on the page should be moved to its own section towards the end, similar to how the page on skeleton is organized.
Some of the back story and the beginning of the merger of the HoTT wiki into the nLab can be gleaned from the original thread.
This was a major event and a fair bit of headache for several weeks. (For me anyways, the so-called “steering committee” may not even have noticed anything.)
Thanks, Madeleine. I assume there was a good reason for it. Perhaps all those “Anonymous” edits, that water down the quality of the nLab generally, had something to do with it.
(Generally, there’s no end to the number of entries one can generate through the semi-mindless exercise of writing ordinary prosaic definitions and propositions in this fashionable language. More real contentful mathematics, please.)
Getting back to the current page: the “Theorem” (I’d sooner demote it to Proposition) is a special case of something extremely general throughout mathematics: if is any binary predicate, then a reflexive transitive relation can be defined by the formula . It goes under many names.
moving Theorem 3.1 and its proof from specialization order to preorder because the proof applies to all binary relations, not just that of the membership relation between elements and open sets of a topological space.
Please identify yourself, Guest, with a name or pseudonym that enables us to distinguish you from other “Guests”.
We have had a problem on many other pages with anonymous editors adding unnecessary type-theoretic stuff. I wish that I had the time to go through and fix all these pages myself, but I just don’t. In any case I agree with Todd: there’s no purpose to rephrasing an essentially foundation-independent definition in type-theoretic language. It’s worth including discussion of alternative foundations when the difference matters, but in this case there’s no evidence presented that it does matter. So I would suggest the section be simply removed from this page.
the text in the dependent type theory section used to define the membership relation is a duplicate of text found in topological space, so I replaced the duplicated text with a link to the topological space article.
Raymond
1 to 20 of 20