Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. 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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2022

    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).

  2. If so, are there any plans to merge the HoTT wiki into the nLab in the near future?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2022
    • (edited Jun 6th 2022)

    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:

    1. the HoTT web is regarded as deprecated,

    2. all further HoTT-related editing should happen on the main nLab web,

    3. anyone who feels like porting an entry or two from there to here would do a great service to the community.

  3. I have added a message on the HoTT web HomePage: https://ncatlab.org/homotopytypetheory/show/diff/HomePage

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2022
    • (edited Jun 7th 2022)

    Dear Madeleine,

    do you know the anonymous person who is currently doing all the edits? It was useful at the beginning, but now they are going astray (here, here, here, here, here, here, here).

    If you know who this is, please ask them to stop with this activity.

  4. 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.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2022
    • (edited Jun 7th 2022)

    Thanks, Madeleine! Much appreciated.

  5. Urs,

    By the way, my name is spelled “Madeleine” with an “e”.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2022

    I see, sorry. Have fixed it now!

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJun 8th 2022
    • (edited Jun 9th 2022)

    From the edit here it looks like the user causing the issue from #7 is some Ali.