Talk:Homotopy type theory

A Special Year

Hello, I'm not entirely sure what is constituted here by the special year on univalent mathematics. The section doesn't do anything to explain what this program constitutes or why it should be interesting to a reader of the encyclopedia. If we wish to keep this as a separate section, we should develop it further so that this is clear. Otherwise, I think the relevant information (that is, an explanation of the discoveries made and perhaps a link to the book) should be merged into other sections of the text. I don't think it's necessary to provide a list of participants or reviews of the work, as this is very unusual for wiki entries on mathematics topics.

I'm happy to spearhead the fleshing out of this section so it makes sense to readers who aren't involved, assuming people can point me in the correct direction for source information. A brief bit of cursory search queries on the topic have returned me to either this entry or the IAS website, which suggests the existence of a weekly seminar and a few working groups but little else. William Of Orange (talk) 17:40, 26 August 2016 (UTC)

Commercial article?

Is it appropriate for an article to become what is in effect an advert for a book, by showing the front cover of the book? If it is felt that a picture would make the article more attractive, an appropriate diagram would do just as well. --Brian Josephson (talk) 19:03, 19 August 2020 (UTC)
A search has revealed that though Amazon keep quiet about this (maybe a Kindle version isn't available), the book is available free so in that sense the article is not commercial. There is very little indication of this in the article, though it turns out that ref. 27 takes you to the page from which the book can be downloaded. The article should give proper indication of its existence. --Brian Josephson (talk) 19:22, 19 August 2020 (UTC)

The book pdf is on github, and anyway we have tons of articles about books that contain a cover pic. 2601:648:8200:990:0:0:0:720 (talk) 19:07, 13 January 2023 (UTC)

Is the cover pic as visible as it is in this article though? Can you give an example? --Brian Josephson (talk) 20:06, 13 January 2023 (UTC)

It would be much nicer to feature a relevant diagram instead of a boring (sorry) book cover. Zaslav (talk) 01:41, 2 December 2023 (UTC)

Too specialized

This article has nothing in it that a non-specialist mathematician can understand. It needs at least a more broadly comprehensible introduction. What are main ideas of HoTT in non-specialized language? What is the purpose of HoTT? What is it used for? Zaslav (talk) 01:47, 2 December 2023 (UTC)

I agree, the introduction could be made more accessible. I think, the HoTT connects and contributes at least to the following fields of research:

• future new foundations of mathematics beyond set theory, in particular "uniqueness up to isomorphism"
• advances in automation of theorem proving (Martin-Löf Type Theory)
• connecting this with the homotopy hypothesis, suggesting a perhaps more suitable equality/identity.

What it makes writing a good introduction difficult, but worth reading, might be the fact, that quite some "corresponding" concepts from seemingly unrelated topics come together here. See the article computational trilogy. Now since each of these correspondences has its own story, balancing such an introduction well is certainly not simple.

The audience for such an introduction would be, beside people with a background in mathematics, those from computer science and philosophy, i think.

-- Cobalt pen (talk) 02:08, 21 December 2024 (UTC)

Section Type equivalence

The section is confusing at best. Most important, it does not follow definions 2.4.1 (homotopy) and 2.4.11 (equivalence) from the HoTT book. Instead it claims "One generally assumes the function extensionality axiom" (i.e. 2.4.1, which is not assumed, but rather a consequence of the UA, see 4.9) and confuses homotopy with identification defining equivalence. -- Cobalt pen (talk) 00:40, 20 December 2024 (UTC)

I'll try to be bold and fix it myself. Please be so kind to review it. I hope, it became a bit better. Please have a particular close look at my cite of Awodey's $\infty$-isomorphism. I'm wavering a bit here, since i feel, that mixing different notations and concepts confuses the notion of identity to be presented more then it helps. Awodey notes about the co-inductive nature of the definition. Perhaps one can add a line or two about this point. -- Cobalt pen (talk) 14:03, 25 December 2024 (UTC)