# Start a new discussion

## Not signed in

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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorAlizter
• 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.
• CommentAuthorAlizter
• 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!

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.
• CommentAuthorAlizter
• 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.
• CommentAuthorAlizter
• 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 \hookrightarrow S^1 \to S^1$ The real Hopf fibration (nlab)
2. $S^1 \hookrightarrow S^3 \to S^2$ The usual complex Hopf fibration (nlab)
3. $S^3 \hookrightarrow S^7 \to S^4$ The quaternionic Hopf fibration (nlab)
4. $S^7 \hookrightarrow S^15 \to S^8$ The octonionic Hopf fibration (nlab)

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

• 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:

• For $S^1$ Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.
• For $S^3$ Buchholtz and Rijke solved this early 2016 through a homotopy version of the Cayley-Dickson construction

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.
• CommentAuthorAlizter
• 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.
• CommentAuthorAlizter
• 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.
• CommentAuthorAlizter
• 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.
• CommentAuthorAlizter
• 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]]


  [[homotopytypetheory: James construction]]

• CommentRowNumber18.
• CommentAuthorAlizter
• 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.
• CommentAuthorAlizter
• CommentTimeAug 5th 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 5th 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.