Talk:Homotopy type theory/Archive 1

mdnahas

Full disclosure: I'm Michael Nahas and I'm a visiting associate at IAS for the spring semester of the Univalent Foundations program. I'm a very minor person in the program. I know Wikipedia prefers people completely unassociated with a topic, but I doubt you'll find anyone who knows this topic who isn't at the program.

mdnahas Mar 2013 — Preceding unsigned comment added by Mdnahas (talk • contribs) 15:04, 2 March 2013 (UTC)

Univalence axiom

I propose that Univalence axiom be merged here. It is only relevant to this topic. May I suggest that you (the primary author) merge other articles that you may have created here, as well. The article is not long, and (IMO) not likely to become wrong. I could be wrong: it could end up being the new category theory, in which I also find little value, but it seems popular. — Arthur Rubin (talk) 20:06, 24 July 2014 (UTC)

History

Regarding the history section: it's a bit misleading to say that Russell proposed Type Theory as an alternative to Set Theory. Not only does Russell's Type Theory predate ZFC, but it was also dominant for a good while. Gödel, Henkin, and Tarski worked their magic in Simple TT. Things only changed over to ZFC as the preferred foundation much later. Anyway, not objecting to the general picture, just to the impression one might get that ZFC was the dominant foundation and then Russell came along and proposed an alternative...

There are many points on which the current article is misleading. However, Russell's theory of types was proposed as an alternative to naïve set theory and Cantor's theory was of course well known. The inclusion of Russell is not particularly relevant though because type theory as it is currently practiced has very little to do with Russell's efforts, especially in the case of Homotopy Type Theory. The latter is derived from Martin-Löf's type theory (the article does not even mention him), which in turn is a generalization of Church's theory. It seems that comment about Russell and about ZFC being "hard to translate" (which is not the case exactly and not why type theory is used instead) come from the linked article, which is not a very good source. 72.24.144.239 (talk) 06:08, 28 October 2014 (UTC)

Conflict of interest tag

One editor deeply connected with this theory wrote almost the entire history section. He has repeatedly added citations to his own work and has even deleted mentions of other contributors. For example, he removed the following sentence describing an important contribution to the theory:

A model of a modified fragment of the Martin-Löf type theory that had generating base types, dependent products and dependent sums but no universes was independently discovered by Michael Warren in 2006/2008.

There are 13 mentions (or citations) of Voevodsky, 6 mentions of Steve Awodey, 3 mentions of Per Martin-Löf, 2 mentions of Michael Shulman, 2 mentions of Michael Warren, and no mention at all of André Joyal, Ieke Moerdijk, or Thierry Coquand. A great many people contributed to HoTT. The history needs more balance. A good place to start would be at the nLab Homotopy type theory page.-Toploftical (talk) 20:52, 8 December 2014 (UTC)

Coquand is mentioned in the History section. You simultaneously complain that Warren is mentioned too often and that one sentence mentioning him was removed...? The nLab article doesn't mention much more than is in this article. Are there any specific claims you think are either should be there but aren't, or are but shouldn't? Your current complain isn't particularly constructive (no pun intended). —Ruud 21:02, 8 December 2014 (UTC)

I did not mean to imply that Warren was mentioned too often. He is only mentioned twice–which might be too few. And he is not mentioned in the body of the article. The sentence about him should not have been removed. Sorry I missed the mention of Coquand.--Foobarnix (talk) 22:30, 8 December 2014 (UTC)

The distribution of names in this articles seems to roughly correspond to the distribution of names in the HoTT book. Joyal recently seemed to have given a similar history in a post to the HoTT mailing list (https://groups.google.com/d/msg/homotopytypetheory/JByi48ujeUc/lRlgOOtCQncJ, first paragraph). There might be potential for a conflict of interests here, but I'm not seeing any to be honest. You also haven't offered anything more than hypotheticals. —Ruud 22:46, 8 December 2014 (UTC)

I agree, the likely COI means we need to be extra careful about due weight and a neutral point of view. The main underlying problem is that the field is new enough that there are AFAICT no good secondary sources laying out the history of the topic. Without secondary sources, we can't establish due weight and write the history from a neutral point of view. Without secondary RS, anything we write is synthesis, a judgment call based on primary sources. Ruud Koot mentions the HoTT book, but this a basically a summary, by the conference attendees, of a year-long conference/seminar and is a primary document. Were there any outside reviewers for this book, especially for the bits of history? The Joyal posting is both primary and unreliable; it should have no bearing on this article. My opinion is that this article's history section should be purged of synthesis, cut back to just the most basic uncontroversial facts or removed altogether until secondary sources develop. --Mark viking (talk) 22:06, 14 December 2014 (UTC)

@Mark viking: Note that Foobarnix implies there may be balance issues with respect to attribution within the HoTT group. I think you are more concerned about the relation of the HoTT group to other groups of researchers, but the article currently does not touch upon this topic at all. —Ruud 00:35, 15 December 2014 (UTC)

Thanks for the clarification. Yes, I was talking about sourcing problems for history section of the topic in general. But given the lack of secondary sources for within-HoTT-group history, it is a problem there, too. I don't think a group of primary researchers, writing a summary in book form about their own very recent work, could be considered a secondary source. --Mark viking (talk) 01:11, 15 December 2014 (UTC)

For nearly all our articles that are slightly more technical we have to rely on survey articles written by those intimately involved with the field for sourcing. Especially given its long list of authors, I think the HoTT book would thus be an acceptable source for its own history. —Ruud 21:35, 17 December 2014 (UTC)

In reply to Ruud's comment about the distribution of names matching that in the book, let me point out that the contents and citations of the HoTT book should not be regarded as limiting or representing the subject as a whole. The book is only about a particular subset of the field of homotopy type theory, namely its use as a foundation for (existing and new) mathematics. The book doesn't even touch on the construction of models, for instance, which is an essential part of the subject and was in fact the first aspect of the subject to be developed (by Awodey and his students first, and then a bit later by Voevodsky). The book's title Homotopy type theory: univalent foundations of mathematics was intended to suggest this: at the time it was chosen, we considered "univalent foundations" to be a good name for the part of the subject which the book covers. (Voevodsky has since decided he wants to take "UF" in a possibly-other direction, so we may have to re-title the book for its second edition.) We imagined there might be other books about other parts of the subject such as Homotopy type theory: categorical semantics or Homotopy type theory: homotopy theory of computation. Michael Shulman (talk) 08:44, 22 December 2014 (UTC)

Proposed merger of Univalent foundations

These two pages cover much of the same material. The person most associated with Univalent foundations has himself said that UF is certainly a subfield of HoTT. The subject is very technical–it will be difficult to maintain one good page about HoTT. Moreover, the UF page badly needs trimming. Many of the citations are obscure and, in some cases, just lead to other citations. It would be difficult for an ordinary mathematician to understand the UF page much less the average WP reader.--Foobarnix (talk) 14:44, 14 December 2014 (UTC)

• Oppose The two topics seem sufficiently different in scope to me (one an alternative type theory, one an alternative foundations of mathematics) that they warrant distinct articles.

To my knowledge (and as I'm merely and interested outsider, please don't take this as a definitive history) UF is a research program instigated (and primarily developed?) by Voevodsky that predates HoTT. HoTT began as an offshoot of UF that both attracted a much larger group of researchers and developed in a different direction than was the original intention of UF. Given this I think there is some merit in having two separate articles as well. —Ruud 15:46, 14 December 2014 (UTC)

Changed to support as I'm mostly in agreement with what Foobarnix said on my talk page: the terms are too often used synonymously, for us to demarcate between them. Having two articles may then only create more confusion than it resolves. I think a terminological note as can be found here or here (although the definitions in the latter may be now be slightly outdated) would be important to have in the lede. —Ruud 21:31, 17 December 2014 (UTC)

I must comment on the sentence in the talk page which states "I strongly believe that Coquand considers himself to be contributing to HoTT, not to Voevodsky's fork", since my name is explicitly mentioned there. In my mind, Voevodsky is one of the main originator of the field, which really started after his formulation of the axiom of univalence, and his insight that notions from homotopy theory can be expressed formally in a direct way in type theory. So it seems to me simply incorrect to represent the univalent foundation program as a "fork" of HoTT, and I see my work as contributing to the univalent foundation program of Voevodsky. I also want to stress that it is a unique opportunity to have a description in wikipedia from one of the main originator of the field.Thcq (talk) 10:00, 19 December 2014 (UTC)Thcq

• Oppose The "person most associated with Univalent foundations" is Vladimir Voevodsky who writes these words. I have never said that UF is a subfield of HoTT. It is not a subfield of HoTT. Vladimirias (talk) 17:33, 20 December 2014 (UTC)

• Support Vladimir, could you provide some evidence that UF is not a subfield of HoTT? Of all the various things I've heard you say at various times that you want "UF" to mean (including the description currently on the wikipedia page Univalent foundations), all of them seem to me to be subfields of HoTT. What does UF include that HoTT doesn't? Michael Shulman (talk) 19:43, 20 December 2014 (UTC)

• Support I'd be OK with a merge. Univalence axiom was already merged here. Univalent foundations seems to be an offshoot of homotopy type theory. The Univalent foundations article suffers from the same likely heavy COI editing issues, by the same editor, as noted in the previous section--if Univalent foundations remains separate, it needs some cleanup and possibly re-balancing. --Mark viking (talk) 20:47, 14 December 2014 (UTC)

• After further consideration, I still support a merge, but for different reasons. It is a fact that there are (IHMO fairly minor, but not insignificant) disagreements among researchers in the field about scope, direction, terminology, etc. In such a case, the role of WP should not be to take either side, but to represent both sides fairly. At present I believe that Vladimir and I have both been at fault in trying to make WP conform to our points of view. At the same time, I think it will be much easier to describe the two fields, their relationship (both historical and present), and the relevant issues, if it is all on one page. In particular, since one of the disagreements has to do with the meaning and relationship of the phrases "homotopy type theory" and "univalent foundations", having two separate pages with these names is an invitation to having them promote divergent points of view. On the other hand, merging them both into one page titled "homotopy type theory", as originally proposed, is itself taking a position; so I propose instead re-titling the merged page in a more neutral way such as "Homotopy type theory and univalent foundations".

  I have started a draft in my userspace here of such a merge. For now, I have attempted to include all the text from both pages that anyone feels to be important; it is probably true that there is too much technical detail (or at least the detail is not explained comprehensibly for the lay reader), but once we have a page that is NPOV and everyone agrees to be at least not wrong, then we can worry about trimming it. (I did rearrange some of the material, e.g. I felt the discussions of h-levels and coherence did not belong in a "History" section.) If I inadvertently left out something important, please consider it just an honest mistake on my part and add it back in an appropriate place. I also tried to be neutral with respect to terminology, e.g. I mentioned both the "h-levels" and "n-types" terminology and tried to give them roughly equal weight. If anyone feels that what I wrote is not sufficiently neutral, please try to make it more neutral. Michael Shulman (talk) 23:31, 12 February 2015 (UTC)

• Oppose A leading expert on UF has stated that it is not a subfield of HoTT and recommends a separate page for it, so maybe we should follow his advice (even if this conflicts with wikipedia policy about experts.) r.e.b. (talk) 01:54, 13 February 2015 (UTC)

To editor R.e.b. - I note that you have added your opposition to this merge proposal with the comment, "A leading expert on UF has stated that it is not a subfield of HoTT and recommends a separate page for it." This expert is VV and he already voted. If you look at the votes so far, everyone except VV supports the merge. If you are basing your opposition on VV's opinion, you are basically giving him two votes.

Do you oppose the merger for reasons other than deference to the opinions of VV?--Foobarnix (talk) 15:37, 13 February 2015 (UTC)

Note that in my last comment I argued for a merge for reasons that have nothing to do with the fact of the matter (insofar as there even is one) about whether or not UF is a subfield of HoTT, which is the only argument against the merge that VV advanced above. Michael Shulman (talk) 17:17, 13 February 2015 (UTC)

• Oppose I don't have any background in this area and I cannot tell whether a merger is a good idea or not. Does my vote count then? If we weight votes according to expertise, then it seems VV's vote settles the matter. If the expertise doesn't count, then my vote should count. My reason for the opposition is the deference to experts. If the primary source (i.e., VV) clearly indicates a distinction between two fields (which he did), the merger is inappropriate. -- Taku (talk) 12:57, 16 February 2015 (UTC)

On what do you base your characterization of VV as "the" primary source, or as having sufficient "expertise" to outvote all the other experts? The fact that people seem to think VV is the only one whose opinion about the field matters is one of the things that makes me strongly oppose having any page on WP that is written only from his POV, as it would only exacerbate that tendency. Michael Shulman (talk) 17:12, 16 February 2015 (UTC)

Also, please read my reply to R.e.b. above. Michael Shulman (talk) 17:15, 16 February 2015 (UTC)

• I change my vote to Oppose. No progress has been made on this issue for some months, and mediation has been rejected. So in the interests of community harmony and progress, I believe it is better to have two separate pages that we can focus our efforts on improving, rather than continue to argue about whether there should be one or two pages. -- Michael Shulman (talk) 22:40, 21 May 2015 (UTC)

History of HoTT and Wikipedia policy

response to above remarks by Coquand

At homotopytypetheory.org we find the paragraph:

Univalent Foundations of Mathematics is Vladimir Voevodsky’s new program for a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory. The type theoretic univalence axiom relates propositional equality on the universe with homotopy equivalence of small types. The program is currently being implemented with the help of the automated proof assistant Coq. The Univalent Foundations program is closely tied to homotopy type theory and is being pursued in parallel by many of the same researchers. [emphasis added]

This is contrasted with the definition of Homotopy Type Theory shown on the same page.

Voevodsky’s has said (e.g., in his Bernays lectures) that

1. he will "distance" himself from HoTT

2. he won't work on "synthetic homotopy theory", which is what a lot of the HoTT people are doing (this includes finding simpler proofs for the theorems of homotopy. On the contrary, he going to work only with hSets (level 0 of the h-hierarchy).

In short, of the things he did bring to HoTT, he's not interested in pursuing them. Rather he's going to work with a small portion of HoTT, with the goal of re-doing his proof of the Milnor conjecture in that small part.

As far as having "a description in wikipedia from one of the main originator of the field", that is actually against Wikipedia policy. See Wikipedia:Verifiability#Reliable_sources where it says

Base articles on reliable, third-party, published sources with a reputation for fact-checking and accuracy. Source material must have been published, the definition of which for our purposes is "made available to the public in some form". Unpublished materials are not considered reliable.

who writes the history

We are indeed fortunate in having Voevodsky helping to write the history of HoTT (along with others who were involved in its creation). Other forums in which the creators themselves write that history may be appropriate, but Wikipedia is not the place to do it. Among many other issues involved, there is the question of conflict of interest. I twice labeled Voevodsky’s Univalent foundations article (he wrote all of it) with a conflict of interest tag but someone immediately removed it.

There is an important larger issue involved. Statements made in WP may be picked up by other medea, repeated endlessly, and finally be considered the true facts of history. Sometimes WP articles have been known to cite sources who themselves used WP as their source! This is called circular reference. See Wikipedia:Verifiability#Wikipedia_and_sources_that_mirror_or_use_it

One of the more germane comments was made above by WP user:Mark viking when he points out that in such a new subject (as HoTT is) there are no good secondary sources. He goes on to say, “My opinion is that this article's history section should be purged of synthesis, cut back to just the most basic uncontroversial facts or removed altogether until secondary sources develop.” He may be right.

new version of the history

The history as currently written is just plain wrong.

Having outlined my view of the current situation, I am going to simply substitute the entire history section with a new version which if believe to accurately reflect that history. It is extensively footnoted. As it exists, it is obviously too long, overly technical, and perhaps even incomplete. I leave it to others to clean it up. But I feel strongly that it is unacceptable to let current inaccurate statements in the article stand become part of the historical record.--Foobarnix (talk) 18:58, 20 December 2014 (UTC)

Addition of Technical Template

I again added this template because the article is becoming increasingly bloated and recondite. For example:

"Even the definition of the model of TS in the homotopy category is non-trivial ... referring to the complex coherence issues that were not resolved until 2009."

Even the mathematician reader may be puzzled by what this coherence is. And no links are given so that the reader can track down what is meant, IAC the entire issue of coherence is too arcane to be mentioned in this history. Another example:

"HoTT uses a modified version of the Propositions as Types interpretation of type theory, according to which types can also represent propositions and terms can then represent proofs."

But if one really wants to trace out the history of this idea, it would have to say something like: "Such a modified version of the Propositions as Types interpretation (in the context of extensional type theory) was perhaps first studied in the language NuPRL, and later in work by Pfenning, Aczel and Gambino, and Awodey and Bauer." Where does this stop?

Some of the editors are treating this article as if it were a mathematical journal article. WP is not the place to explain the nuts and bolts of basic research.

See Wikipedia is not a publisher of original thought

Also see :Wikipedia is not a manual, guidebook, textbook, or scientific journal

--Foobarnix (talk) 18:37, 4 January 2015 (UTC)

Thanks for making this point! I think there are some of us working in the field who would like to record and "get straight" the early history of the subject, but it's good for us to be reminded that WP is not really the right place for that. Michael Shulman (talk) 06:20, 5 January 2015 (UTC)

The special year section

The section on the special year is imbalanced because it speaks mostly of the HoTT book, and so it gives the impression that this was the only thing we did. The section should actually say that the Special year was a catalyst for the development of the subject, and that the book was only one (perhaps most visible) result. Also, the history section is gettting awfully detailed, as well as unverified by Wikipedia standards (correct me if I am wrong). Frege (talk) 07:56, 5 February 2015 (UTC)

Applications

The section on applications is far from being clear. f someone could improve that section, it would be great. — Preceding unsigned comment added by 175.214.164.29 (talk) 16:05, 27 February 2015 (UTC)

Univalence Foundations Section

I have removed the following text from the article page

"(Voevodsky has tried) to reserve the term "univalent foundations" for those that involve his own research, such as the UniMath library of formalized mathematics. It remains to be seen whether this usage will become dominant."  

These statements are incorrect. In particular, the only statement with any support in the form of a reference to my Bernays lectures misinterprets what I have said - my words were not about my intentions in general but about the development of the UniMath library that I saw moving more in the direction of formalization of classical mathematics. In practice however UniMath still remains a library of formalized constructive mathematics (we have never used the excluded middle axiom in the library so far) so even this reading is misleading.Vladimirias (talk) 15:49, 20 January 2016 (UTC)