Talk:Univalent foundations

Cubical type theory

I removed the following sentence:

It is expected that in the near future the underlying formal deduction system will evolve probably in the direction of cubical type theory.

It is not stated who expects this. The citations supplied (which do indeed discuss cubical type theory) do not mention anyone anywhere who said this. If there is an authoritative source for this statement, please cite it.

--Foobarnix (talk) 15:01, 11 December 2014 (UTC)

Proposed merger of Univalent foundations

The Merge template was added because UF is a subset of Homotopy Type Theory. The term Univalent foundations is associated with Vladimir Voevodsky. It is not clear from the article, which Voevodsky himself wrote, in what way this term differs from HoTT. Or indeed, exactly what he means by UF. His definition has changed over time.

The HoTT page at nLab contains the statement "As a foundation for mathematics, homotopy type theory (also called univalent foundations)..." If Univalent foundations and HoTT are the same thing, we do not need two articles. Most researchers do not appear to regard them as separate subjects.

I would also point out that the special year on the Univalent Foundations of Mathematics at the Institute for Advanced Study organized by Awodey, Coquand, and Voevodsky resulted in a book which launched a new subject titled, Homotopy Type Theory, Univalent Foundations of Mathematics . So, at that time, even Voevodsky seems to be agreeing that they are just one subject. If VV has since forked HoTT into a new subject, that needs to be explained clearly.

--Foobarnix (talk) 17:18, 14 December 2014 (UTC)

Reasons for merging UF into HoTT

There has been no clear statement of how Univalent foundations is not included in Homotopy type theory. Much of the information in both articles is repetitious, overlapping, and–in some cases–contradictory. Having one article about such an arcane and (apparently) controversial subject is already hard enough to maintain. Two such articles will be impossible to keep in sync. Adding to the difficulty of maintaing two articles is the fact (as pointed out by editor Mark viking) that the whole subject at present is a bit skimpy on secondary sources.

Having two articles about the same subject is against several Wikipedia policies. See Redundant articles, Article creep, and also note the following two points found on the page Wikipedia:List of bad article ideas:

5. A second article on an existing topic; you can just edit the existing article.

12. A new article to supplement an already existing one which you think is not putting your point across forcefully enough.

--Foobarnix (talk) 16:39, 17 February 2015 (UTC)

Main Concepts

The claim that "classical mathematics is considered to be a "retract" of constructive math (together with the use of the "quotient" (in quotes), are descriptions that can be understood only by mathematicians. No links to definitions are given. These lines don't belong in a WP article. See Wikipedia is not a publisher of original thought.

The material on h-levels is too technical for a general, introductory article such as this. It should be removed. WP is not a textbook. See Wikipedia is not a manual, guidebook, textbook, or scientific journal.

No, the material on h-levels is not too technical for a general, introductory article such as this. Take a look at the definition of 2-category and compare it to the definitions presented here, which explain, in just a few words how type theory "includes" propositional logic and set theory. -- User:DanGrayson

Material removed from UF article

Most of this Univalent foundations (= UF) article was written by editor Vladimirias. Vladimirias is Vladimir Voevodsky (=VV), one of the principal researchers in Homotopy Type Theory (= HoTT). Along with Steve Awodey, Thierry Coquand, Andrej Bauer and others, VV organized A Special Year on Univalent Foundations of Mathematics at the Institute for Advanced Study in 2012-13.

Some of the remarks below refer to the Paul Bernays Lectures which Vladimir Voevodsky gave in 2014:

• video of lecture 1
• video of lecture 2
• video of lecture 3

Confusingly, the term "univalent foundations" has come to be used in two senses.

• In its wider sense it is synonymous with Homotopy Type Theory (HoTT). Indeed, the subtitle of the HoTT book is "Univalent Foundations of Mathematics".
• Its narrower sense, due to the insistence of Vladimir Voevodsky, refers to:

1. The parts of HoTT-UF due to him.

2. The libraries he has and will continue to create, now referred to as UniMath library.

Moreover, VV has announced, in his third Bernays Lecture (at about 39 minutes into the talk) what he will now work on. His interest is in the formalization of classical math, in particular his proof of the Milnor conjecture, as opposed to "the new stuff they're doing" (mainly synthetic homotopy theory), using only the UF version of Set Theory (his "h-level 2"), with some h-level 3 when necessary, and allowing himself the Axiom of Choice and (hence) Excluded Middle.

The first sentence has been stricken, because

• The reader has no way of knowing what the quoted phrase "univalent types" means.
• The reader cannot understand what's meant by "structures that correspond, under the projection to set-theoretic mathematics, to homotopy types" without having absorbed a large part of the the UF theory. In particular, just what is the projection that's referred to? Perhaps the author, VV, is trying to express something that he states somewhat more clearly elsewhere, and that relies crucially on the concept of h-level; namely, on Slide 8 of his third Bernays lecture he says that "types of all h-levels appeared in the set-level mathematics in the form of homotopy types". In the lecture itself he carries this further by saying (at 23 min into it) that "homotopy types are kind of reflections in the set-level math of types of higher levels". So he seems to be saying that the types of UF are homotopy types, and, at the same time, that homotopy types are just the set-level reflections of the types of UF. Surely this apparently contradictory nebulosity, that occurs only at a late stage in his own lectures, is not appropriate as an opener for an article on UF.

The second sentence, on the inspiration for univalent foundations, has been stricken, because

• The only reference given is the author's own Bernays lectures.
• Those lectures contain no references to "the old Platonic ideas of Hermann Grassmann and Georg Cantor". Indeed, the lectures practically contradict this claim. First, Plato isn't mentioned. Second, the author tells us how impressed he's been by the ideas of the Neo-Platonic philosopher Proclus. But Neo-Platonic is not Platonic (indeed, some have held them to be quite opposed). Third, VV says he has read Proclus only during the past year. But his ideas for the UF were developed several years before that, so Proclus cannot have been their inspiration. As for Grassmann's Ausdehnunglehre, of which VV claims to have read only the introduction, the ideas discussed seem to have nothing to do with UF except by way of a dubious doctrine of "shapes": that by "forms" Grassmann means shapes, and shapes = homotopy types, which would strike the generic person as a huge stretch, and that homotopy types = the types of UF, which is just false (as pointed out on p 3 of the HoTT book and, more explicitly, on p 290).

The fourth sentence has been stricken because

• Its claim that "the development of the univalent foundations is closely related with the development of homotopy type theory" gives the impression that these two (if they are two) theories have been far less intimately related than is the case.

History section

• The first sentence omits the relation of the "main ideas of univalent foundations" to those of HoTT.
• In the article Vladimir Voevodsky VV himself has written.

In 2009 he constructed the univalent model of the Martin-Löf type theory in simplicial sets. This was a major step in the development of homotopy type theory, and led to his programme of using it as a foundation for all mathematics. In such a role he calls it univalent foundations.

• See Wikipedia is not a soapbox or means of promotion

--Foobarnix (talk) 15:39, 9 February 2015 (UTC)

Too technical tag added

In addition to various undefined terms such as "cubical type theory" many of the statements in this article cite technical blogs which will not be understandable by the reader. Moreover, some of the blogs cited are written by VV, so they are not really citations to secondary sources. See Wikipedia:Verifiability Self-published_sources.

--Foobarnix (talk) 15:38, 9 February 2015 (UTC)

The introduction

The first sentence currently says this:

In foundations of mathematics, univalent foundations is an approach to the foundations of mathematics based on the idea that mathematics studies structures on "univalent types" that correspond, under the projection to set-theoretic mathematics, to homotopy types.

There are some problems with this sentence:

• the phrase "homotopy type" has no clear meaning: it doesn't refer to a type of mathematical object in informal mathematics, but rather, to a way of discussing a type of mathematical object in a formal language that doesn't yet exist. And the link given for clarification goes to the Wikipedia page on Homotopy, which doesn't address the modern usage, and doesn't even define the classical term (as an equivalence class of spaces under homotopy equivalence), which is not intended here.
• the phrase "univalent types" is undefined, here and elsewhere. It seems to occur only here. The usual phrase is "univalent universe".
• it's not clear what is meant by "projection". To clarify that would involve discussion of Voevodsky's interpretation of the terms of the language in topology, whose construction depends on unpublished papers and the unproven "initiality conjecture"

After discussion with others, I'd like to change it to this:

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called "types". Types in the univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path.

Daniel R. Grayson (talk) 12:50, 9 April 2018 (UTC)