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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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).

nLab: Seperate open problems page for homotopy theory in HoTT.

Bottom of Page

1 to 24 of 24

  1.  
    • CommentRowNumber1.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)
    Should we create a seperate page for open/solved problems about algebraic topology in HoTT. There is already discussion of clutter on the open problems page, this would reduce clutter and make it clearer for people interested in doing homotopy theory in HoTT. This would make the open problems page more of a meta problems, but thats okay.

    This page would essentially survey results about algebraic topology in HoTT and homotopy groups calculated in HoTT.

    I imagine an algebraic topologist who is interesting in doing homotopy theory, would find this page very useful with all known and used constructions etc.

    Is anyone else in favour of this change?
    • CommentRowNumber2.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)
    I have started a page https://ncatlab.org/homotopytypetheory/show/Homotopy+theory+in+HoTT.
    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)

    I applaud that you invest energy into this!

    A general hint on hyperlinks:

    For making general hyperlinks at the nForum appear, type

      [link text](url)

    while making sure that below the edit pane you have selected “Markdown+Itex”

    For links to entries on a web belonging to the nLab, you may also type

      [[webname:entryname]]

    for instance

      [[homotopytypetheory:Homotopy+theory+in+HoTT]]

    produces

    Homotopy+theory+in+HoTT (homotopytypetheory)

    Finally, if the entry is on the main nLab web, you may omit the webname and just type

      [[James construction]]

    to produce

    James construction

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 5th 2018

    Do you mean would such a page be welcome on the nLab rather than the HoTT web? I’d say certainly yes. One advantage is that you wouldn’t have to worry about filling in basic links, such as to torus.

    Perhaps we might look to rationalize our pages here. We have related pages:

    • CommentRowNumber5.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)
    I have made a new page: Hopf fibration (homotopytypetheory) and H-space (homotopytypetheory). One note about the overall nlab, can we reduce homotopytypetheory down to hott in the web links?
    • CommentRowNumber6.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)
    David one problem I am having trouble with is that some constructions in HoTT really don't care about the classical stuff. Take for example pushouts: doing pushouts in HoTT feels a lot more different then the longer definitions in classical algebraic topology. Perhaps it is a good idea to seperate them but obviously have links between.

    ---
    Edit:
    Ignoring the blabbering above: Say for the torus, we should have a link in a HoTT section linking it to the definition(s) of a torus in HoTT.
    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 5th 2018

    The homotopytypetheory web isn’t usually discussed at the nForum, and most of its contributors won’t see messages here.

    You might wonder if it’s worth the effort. The web only has 62 pages compared to over 13000 here. But, of course, if you want to develop it as a purely HoTT wiki, then I can’t think any one will want to stop you.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)

    Let’s do make sure to at least have links between the entries.

    I just did some cross-linking for Hopf fibration:

    the beginning of Hopf fibration (homotopytypetheory) now reads as follows:

    In classical algebraic topology (nlab) we have four Hopf fibrations (nlab) (of spheres):

    1. S 0↪S 1→S 1S^0 \hookrightarrow S^1 \to S^1 The real Hopf fibration (nlab)
    2. S 1↪S 3→S 2S^1 \hookrightarrow S^3 \to S^2 The usual complex Hopf fibration (nlab)
    3. S 3↪S 7→S 4S^3 \hookrightarrow S^7 \to S^4 The quaternionic Hopf fibration (nlab)
    4. S 7↪S 15→S 8S^7 \hookrightarrow S^15 \to S^8 The octonionic Hopf fibration (nlab)

    while the end of Hopf fibration (nlab) now has this line:

    For more discussion in homotopy type theory see also at

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)

    Alizter, I have another request: Please try to provide decent references.

    Currently at Hopf fibration (homotopytypetheory) it has the following:

    This is bad style. One would never cite in such a sloppy way in a research article, and for a good reason.

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 5th 2018

    Re #6, there’s plenty of sympathy expressed through nLab pages to the thought that homotopy theory is more basic than its classical manifestation. Entries often include sections expressed in HoTT, see for instance at infinity-action.

    It would be great to have a HoTT section at torus.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018

    I have harmonized the formatting of the citation to Buchholtz-Rijke 16 now.

    This makes me realize that the homotopytypehteory web does not share with the main nLab the functionality that anchor targets get highlighted in gray, so that one maydiscern which reference is actually being pointed to. Does anyone know how to copy that functionality over?

    • CommentRowNumber12.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    After some thinking I think I agree that it is a pointless and wasteful endevour to develop the HoTT wiki outside of nlab. So I propose the following: I currently have written a few HoTT wiki pages that I think can be merged into their main nlab counterparts.

    As for bad style, I had copied that from the open problems page on the HoTT wiki.
    • CommentRowNumber13.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)
    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)

    After some thinking I think I agree that it is a pointless and wasteful endevour to develop the HoTT wiki outside of nlab. So I propose the following: I currently have written a few HoTT wiki pages that I think can be merged into their main nlab counterparts.

    I think that’s a great idea.

    As for bad style, I had copied that from the open problems page on the HoTT wiki.

    Right, lots of people do that; sorry for targeting that complaint at you.

    What I am trying to express is that it is good to aim for formatting of wiki-pages which is on roughly the same level as one would adopt in research articles. On the nLab have learned this the hard way ourselves, with early entries later feeling like an embarrassment when the public perception of the wiki had grown.

    • CommentRowNumber15.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    Don't worry Urs, I can feel your frustration. That's precisely why I am talking on the nforum because I don't want to dump a load of sloppily written articles at your doorstep.
    • CommentRowNumber16.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)
    Let's begin with James construction (homotopytypetheory) just so I can get a feel about how to edit the main nlab pages.

    ***

    Actually ignore that I need to learn to read first.
    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018

    BTW, the problem with the link in #16 is a spurious whitespace after the colon. It needs to be

      [[homotopytypetheory:James construction]]

    instead of

      [[homotopytypetheory: James construction]]
    • CommentRowNumber18.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 5th 2018
    For H-space (homotopytypetheory) there is a nice wiki page now. How on earth does this get merged into H-space? I am trying to understand because it has all the same sections but if its going to be in its own section these will have to be subsections? How would we go about doing this?
    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeAug 5th 2018

    I think this is not the place to discuss or decide the future of the homotopytypetheory web, such as whether it should be merged into the main nLab web, because the people that it was created by and for do not, by and large, frequent this forum. Please raise that question somewhere else such as the HoTT mailing list, before taking action on it.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)

    Alizter, the H-space on the hoomotopytypetheory wiki has almost no content, beyond a telegraphic definition. The Idea-section there I had just added a few minutes back. So there would not be much to be merged in this case.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 5th 2018

    Re #19, yes, I was just giving reasons why Alizter might prefer to devote his energy to the nLab over homotopytypetheory. It’s not up to us to merge the two webs.

    • CommentRowNumber22.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 6th 2018
    Mike, I did in fact ask the HoTT mailing list. We were not merging any articles that already exist on the wiki, just trying to work out where to write new ones.
    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeAug 6th 2018

    You asked the HoTT mailing list about splitting up the open problems page in particular. But in #12 you called it a “pointless and wasteful endevour” to write pages on the homotopytypetheory wiki rather than on the main nlab, which is a different question. What led you to that conclusion?

    On first thought, I rather like the idea of having (for instance) two separate pages H-space (homotopytypetheory) and H-space (nlab) (interlinked of course), because they are really about different things that have been given the same name, connected by the interpretation of homotopy type theory into classical homotopy theory. I often find that nLab pages become rather unwieldy and hard to navigate when they try to explain on one page many different things that have the same name in different contexts.

    • CommentRowNumber24.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 6th 2018
    • (edited Aug 6th 2018)

    Just a quick suggestion. I think it would be very useful to include code (in as many languages as possible, but at least Coq and Agda) encoding the definition at H-space (homotopytypetheory).

    On a different note, I can treat the HoTT wiki in the same way as the main nLab with regard to forum announcements, etc, should people wish.

1 to 24 of 24

  1.