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.
1 to 12 of 12
Right now the HoTT wiki seems to be de facto an anonymous user’s personal web where they make draft articles before porting them over to the nLab: see i.e. biaction (homotopytypetheory) and biaction (nlab), ETCS with elements (homotopytypetheory) and ETCS with elements (nlab), enriched poset (homotopytypetheory) and enriched poset (nlab), et cetera. Otherwise, there doesn’t seem to be much activity on the HoTT wiki at all. The type theory and homotopy type theory material on the nLab is already much more elaborated than the equivalent articles on the HoTT wiki (see identity type (nlab) and identity type (homotopytypetheory)), and the only user contributing to the HoTT wiki is more interested in their own pet projects in abstract algebra and analysis (i.e. halving group (homotopytypetheory)) than actually expanding on the core homotopy type theory content.
Yes. I have said this a few times before, and more recently other regulars have said it, too.
There should be good synergy effects of having on a single page discussion of both the traditional incarnation of a concept as well as its incarnation in HoTT.
And should it really be necessary/desireable to have stand-alone HoTT pages paralleling pages with traditional content, then that’s easily accomodated for by creating a new nLab page with an appropriate title (say “XYZ (in HoTT)” of the like).
If so, are there any plans to merge the HoTT wiki into the nLab in the near future?
I haven’t seen any plans regarding the HoTT wiki discussed here. (Which is part of the problem of it being a separate web: There is/was no interaction between the communities editing there and here.)
It seems doubtful that a semi-automated merging is feasible, and even if it were, it seems doubtful that we would find a volunteer doing it. (Since we barely have the volunteers for keeping the whole system afloat in the first place.)
Instead, one should proceed by prominently announcing on the HoTT web HomePage that:
the HoTT web is regarded as deprecated,
all further HoTT-related editing should happen on the main nLab web,
anyone who feels like porting an entry or two from there to here would do a great service to the community.
I have added a message on the HoTT web HomePage: https://ncatlab.org/homotopytypetheory/show/diff/HomePage
Urs,
Sorry, I do not know the anonymous person, but it seems that whoever they are doesn’t seem to be reading the nForum or else they would have seen your messages.
I have added a note to the HoTT wiki’s home page about adjusting the material to fit the nLab when copying over pages to the nLab, in hope that the anonymous editor reads the note and gets the message.
Thanks, Madeleine! Much appreciated.
Urs,
By the way, my name is spelled “Madeleine” with an “e”.
I see, sorry. Have fixed it now!
1 to 12 of 12