User:Foobarnix/Article builder 1: Difference between revisions

From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
x
Final version of foobarnix's Arguments for merging UF with HoTT
Line 1: Line 1:
Throughout these remarks I use the abbreviations '''UF''' for Univalent foundations, '''HoTT''' for Homotopy Type Theory, and '''VV''' for Vladimir Voevodsky.

The name of the new merged article would be '''{{Font color|Blue|Homotopy Type Theory and Univalent Foundations}}'''

==Arguments for merging Univalent foundations with Homotopy Type Theory==
1. The special year on the Univalent Foundations of Mathematics<ref>[https://www.math.ias.edu/sp/univalent IAS School of Mathematics: Univalent Foundations of Mathematics]</ref> at the [[Institute for Advanced Study]] organized by [[Steve Awodey]], [[Thierry Coquand]], and [[Vladimir Voevodsky]] resulted in a book titled, ''Homotopy Type Theory, Univalent Foundations of Mathematics''.<ref name=hottbook/> So, at that time, even Voevodsky seems to be agreeing that they are just one subject.

2. One of the principal participants in the HoTT special year [[Michael Shulman (mathematician)|Michael Shulman]] posted the following on 22 December 2014 on the page [[Talk:Homotopy type theory]]:
: 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,<ref>{{Cite journal|url = https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf|title = Structuralism, Invariance, and Univalence|last = Awodey|first = Steve|date = |journal = [[Philosophia Mathematica]]|accessdate = 13 December 2014|doi = 10.1093/philmat/nkt030|authorlink = Steve Awodey|publisher = Oxford University Press|volume = 22|issue = 1|year = 2014|issn = 0031-8019}}</ref> and then a bit later by Voevodsky). The book's title ''Homotopy type theory: univalent foundations of mathematic''s 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.

3. Everyone seems to agree that, at least for the moment, there’s at least a very large overlap between HoTT and UF, but different people use them differently:
: some people such as Shulman consider UF as a subtype/subfield of HoTT
: some people such as Peter Lumsdane use them approximately interchangeably
: some people such as Thierry Coquand and VV see them as overlapping but non-trivially different
: some Wikipedia editors such as [[User:Mark viking|Mark viking]] and former merge opponent [[User:Ruud Koot|Ruud Koot]] support a merge

4. [[User:R.e.b.|Editor r.e.b.]] opposes a merge on the grounds that, "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." I responded to r.e.b. saying, "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?" So far '''r.e.b.''' has not responded.

5. [[User:TakuyaMurata|Editor Taku]] opposes a merge on the grounds saying, "I don't have any background in this area and I cannot tell whether a merger is a good idea or not. If we weight votes according to expertise, then it seems VV's vote settles the matter." Again this is simply deference to VV. Michael Shulman responded to Taku with, "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." So far '''Taku''' has not responded.

6. 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.
In the biographical 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''.

The mediation page was created on 17:08, 22 February 2015. On 18:51, 22 February 2015‎ VV changed this paragraph to say,
:In 2009 he constructed the univalent model of the Martin-Lof type theory in simplicial sets. This led to important advances in the development of new foundations of mathematics that Voevodsky has been working on.--[[User:Foobarnix|Foobarnix]] ([[User talk:Foobarnix|talk]]) 15:23, 23 February 2015 (UTC)

7. The HoTT page at nLab<ref>[http://ncatlab.org/nlab/show/homotopy+type+theory HoTT page at nLab]</ref> (one of the principal forums for discussion of the entire subject) contains the statement:
: As a foundation for mathematics, homotopy type theory (also called univalent foundations) has the following advantages...”
So at least some of the people in this forum see the two subjects as identical.

8. 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''.
* In its narrower sense, due to the insistence of Vladimir Voevodsky, it 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 and Foundations.<ref name=UniMath>[https://github.com/UniMath/UniMath UniMath]</ref><ref name=Foundat>[https://github.com/vladimirias/Foundations Foundations]</ref>

9. Having two articles about the same subject is against several Wikipedia policies. See [[Wikipedia:Avoiding_common_mistakes#Redundant|Redundant articles, Article creep]], and also note the following two points found on the page [[Wikipedia:List of bad article ideas]]:
:point 5. A second article on an existing topic; you can just edit the existing article.
:point 12. A new article to supplement an already existing one which you think is not putting your point across forcefully enough.

10. There has been no clear statement by VV of how Univalent foundations is not included in Homotopy type theory. One of the principal researchers in HoTT, [[Michael Shulman (mathematician)|Michael Shulman]] asked him directly with his posting '''[[Talk:Homotopy_type_theory#Proposed_merger_of_Univalent_foundations|here]]'''
: 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?
:: Significantly VV never answered this question.

11. The pages on HoTT and UF cover the same material. 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 [[User:Mark viking|editor Mark Viking]]) that the whole subject at present is a bit skimpy on [[Wikipedia:No_original_research#Primary.2C_secondary_and_tertiary_sources|secondary sources]].

12. The UF article is written almost entirely by VV. The citations are poorly formatted and not up to WP standards. Many of the citations are to his own Bernays lectures given in 2014<ref name=Bernays1>[https://www.youtube.com/watch?v=ijv3pMU9PAw Bernays lecture 1]</ref><ref name=Bernays2>[https://www.youtube.com/watch?v=BMassUD80mM Bernays lecture 2]</ref><ref name=Bernays3>[https://www.youtube.com/watch?v=4-xEmaGPciQ Bernays lecture 3]</ref> or to blogs written by VV himself.<ref name=UniMath/><ref name=Foundat/> And typical of blogs, many of the citations are already dead links. To fix up these references would be a lot of work and nobody other than VV seems inclined to do it.

As editor [[User:Sławomir Biały|Sławomir Biały]] pointed out when discussing the UF page written by VV, "...we should certainly not allow this niche of Wikipedia to become his personal blog." Biały seemed to feel that this could be fixed but I am not so sure. After all, VV wrote it and he reverted all attempts by me to trim out excessively technical and uncited material. Better to put the whole subject into one article where everybody can focus on it.

13. For a final point I use the following edit by VV. I maintain that this edit history shows that VV is not only insisting on his own definition of UF, but is also willing to delete the edits of other people in order to obscure the fact that there is disagreement among experts about the meanings of the terms UF and HoTT.

[https://en.wikipedia.org/w/index.php?title=Homotopy_type_theory&oldid=646683065 The HoTT page as of 13:51, 11 February 2015] contained the following section which talks about UF:
:;Univalent foundations
:The phrase "univalent foundations" is agreed by all to be closely related to homotopy type theory, but not everyone uses it in the same way. It was originally used by Vladimir Voevodsky to refer to his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant.<ref name=hottcentral>[http://homotopytypetheory.org/ Type Theory and Univalent Foundations]</ref>

:As Voevodsky's work became integrated with the community of other researchers working on homotopy type theory, "univalent foundations" was sometimes used interchangeably with "homotopy type theory",<ref>See especially the Introduction to Homotopy Type Theory: Univalent Foundations of Mathematics</ref><ref name=hottbook>[http://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf Homotopy Type Theory: Univalent Foundations of Mathematics]</ref> and other times to refer only to its use as a foundational system (excluding, for example, the study of model-categorical semantics or computational metatheory).<ref name=hottrefs>[http://ncatlab.org/homotopytypetheory/show/References Homotopy Type Theory: References]</ref> For instance, the subject of the IAS special year was officially given as "univalent foundations", although a lot of the work done there focused on semantics and metatheory in addition to foundations. The book produced by participants in the IAS program was titled "Homotopy type theory: Univalent foundations of mathematics"; although this could refer to either usage, since the book only discusses HoTT as a mathematical foundation.<ref name=hottbook/>

:More recently, Voevodsky has tried to distance himself from certain perspectives on homotopy type theory that he disagrees with, and to reserve the term "univalent foundations" for those that involve his own research, such as the UniMath library of formalized mathematics.<ref name=UniMath/><ref>Voevodski 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).</ref> It remains to be seen whether this usage will become dominant.<ref name=Bernays1/><ref name=Bernays2/><ref name=Bernays3/>

VV in his [https://en.wikipedia.org/w/index.php?title=Homotopy_type_theory&oldid=646863385 edit of 17:55, 12 February 2015] - with no edit summary note - completely rewrote this section as follows:
:;Univalent foundations

:The phrase "univalent foundations" was introduced by Vladimir Voevodsky to refer to his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant.<ref name=hottcentral/>

:When Voevodsky presented his work to the community of other researchers working on homotopy type theory there was, along with much interest in the mathematical constructions that he invented, a common unwillingness and hesitation to support the idea that this can indeed be a new foundation of mathematics. The phrase "homotopy type theory" was chosen instead to emphasize that those working on the subject do not challenge the accepted foundations of mathematics but only develop a new field inside the existing paradigm. The definition of the homotopy type theory given in the HoTT book emphasizes this point of view. Over the last few years as it was becoming clear that the claim that Voevodsky was making has a substance, the phrase "homotopy type theory" started to be used more and more often interchangeably with the univalent foundations as a name for a new approach to foundations of mathematics.

:One of the problems that arose after the special year was the over-emphasis in the presentations related to HoTT on the so called "synthetic homotopy theory". This over-emphasis was creating the opinion among mathematicians less familiar with the details of the subject that the the main uses of HoTT were in formalization of homotopy theory through the use of synthetic constructs such as higher inductive types distracting the attention from the fact that it provided the best available environment for the formalization of the usual set-theoretic mathematics in type theories such as MLTT and CIC. Voevodsky, in particular in his Bernays lectures,<ref name=Bernays1/><ref name=Bernays2/><ref name=Bernays3/> was trying to correct this misconception by emphasizing the possibilities that the univalent foundations presented for the formalization of the ordinary set-theoretic mathematics, including classical mathematics.

This new version by VV contained no citations other than for his own Bernays lectures and also a [http://homotopytypetheory.org/ blog] titled 'Homotopy Type Theory' which then has a subtitle 'Homotopy Type Theory and Univalent Foundations'. Moreover, the page cited says that UF is "...based on the homotopical interpretation of type theory." So even in his own citations VV demonstrates how intimately related the two terms are. Notice also that VV in his edit said, "...the phrase 'homotopy type theory' started to be used more and more often interchangeably with the univalent foundations as a name for a new approach to foundations of mathematics." So is VV arguing against a merge of the two article, or for it?

This edit was immediately reverted by Michael Shulman on 18:28, 12 February 2015 with the comment “That's totally contrary to my memory of events, and also (it seems to me) to the text of the book; it would need to be backed up by citations.”

==Sources of this material==
Many of these arguments have simply been condensed and rearranged from material already in WP. See the following pages:

* '''[[Wikipedia_talk:WikiProject_Mathematics#Vladimir_Voevodsky.2C_univalent_foundations.2C_and_homotopy_type_theory|'Vladimir Voevodsky, univalent foundations, and homotopy type theory]]''' on the page Wikipedia talk:WikiProject Mathematics
* [[Talk:Univalent foundations]]
* [[Talk:Homotopy type theory]]
* '''Related to the Univalent Foundations page''' which was posted by VV on [[User talk:Foobarnix]]
* [[User:Michael Shulman/draft Homotopy Type Theory and Univalent Foundations]] - This is the proposed new draft

==References==
{{reflist}}

Revision as of 22:01, 14 October 2015

Throughout these remarks I use the abbreviations UF for Univalent foundations, HoTT for Homotopy Type Theory, and VV for Vladimir Voevodsky.

The name of the new merged article would be Homotopy Type Theory and Univalent Foundations

Arguments for merging Univalent foundations with Homotopy Type Theory

1. The special year on the Univalent Foundations of Mathematics[1] at the Institute for Advanced Study organized by Steve Awodey, Thierry Coquand, and Vladimir Voevodsky resulted in a book titled, Homotopy Type Theory, Univalent Foundations of Mathematics.[2] So, at that time, even Voevodsky seems to be agreeing that they are just one subject.

2. One of the principal participants in the HoTT special year Michael Shulman posted the following on 22 December 2014 on the page Talk:Homotopy type theory:

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,[3] 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.

3. Everyone seems to agree that, at least for the moment, there’s at least a very large overlap between HoTT and UF, but different people use them differently:

some people such as Shulman consider UF as a subtype/subfield of HoTT
some people such as Peter Lumsdane use them approximately interchangeably
some people such as Thierry Coquand and VV see them as overlapping but non-trivially different
some Wikipedia editors such as Mark viking and former merge opponent Ruud Koot support a merge

4. Editor r.e.b. opposes a merge on the grounds that, "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." I responded to r.e.b. saying, "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?" So far r.e.b. has not responded.

5. Editor Taku opposes a merge on the grounds saying, "I don't have any background in this area and I cannot tell whether a merger is a good idea or not. If we weight votes according to expertise, then it seems VV's vote settles the matter." Again this is simply deference to VV. Michael Shulman responded to Taku with, "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." So far Taku has not responded.

6. 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. In the biographical 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.

The mediation page was created on 17:08, 22 February 2015. On 18:51, 22 February 2015‎ VV changed this paragraph to say,

In 2009 he constructed the univalent model of the Martin-Lof type theory in simplicial sets. This led to important advances in the development of new foundations of mathematics that Voevodsky has been working on.--Foobarnix (talk) 15:23, 23 February 2015 (UTC)

7. The HoTT page at nLab[4] (one of the principal forums for discussion of the entire subject) contains the statement:

As a foundation for mathematics, homotopy type theory (also called univalent foundations) has the following advantages...”

So at least some of the people in this forum see the two subjects as identical.

8. 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.
  • In its narrower sense, due to the insistence of Vladimir Voevodsky, it 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 and Foundations.[5][6]

9. 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:

point 5. A second article on an existing topic; you can just edit the existing article.
point 12. A new article to supplement an already existing one which you think is not putting your point across forcefully enough.

10. There has been no clear statement by VV of how Univalent foundations is not included in Homotopy type theory. One of the principal researchers in HoTT, Michael Shulman asked him directly with his posting here

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?
Significantly VV never answered this question.

11. The pages on HoTT and UF cover the same material. 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.

12. The UF article is written almost entirely by VV. The citations are poorly formatted and not up to WP standards. Many of the citations are to his own Bernays lectures given in 2014[7][8][9] or to blogs written by VV himself.[5][6] And typical of blogs, many of the citations are already dead links. To fix up these references would be a lot of work and nobody other than VV seems inclined to do it.

As editor Sławomir Biały pointed out when discussing the UF page written by VV, "...we should certainly not allow this niche of Wikipedia to become his personal blog." Biały seemed to feel that this could be fixed but I am not so sure. After all, VV wrote it and he reverted all attempts by me to trim out excessively technical and uncited material. Better to put the whole subject into one article where everybody can focus on it.

13. For a final point I use the following edit by VV. I maintain that this edit history shows that VV is not only insisting on his own definition of UF, but is also willing to delete the edits of other people in order to obscure the fact that there is disagreement among experts about the meanings of the terms UF and HoTT.

The HoTT page as of 13:51, 11 February 2015 contained the following section which talks about UF:

Univalent foundations
The phrase "univalent foundations" is agreed by all to be closely related to homotopy type theory, but not everyone uses it in the same way. It was originally used by Vladimir Voevodsky to refer to his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant.[10]
As Voevodsky's work became integrated with the community of other researchers working on homotopy type theory, "univalent foundations" was sometimes used interchangeably with "homotopy type theory",[11][2] and other times to refer only to its use as a foundational system (excluding, for example, the study of model-categorical semantics or computational metatheory).[12] For instance, the subject of the IAS special year was officially given as "univalent foundations", although a lot of the work done there focused on semantics and metatheory in addition to foundations. The book produced by participants in the IAS program was titled "Homotopy type theory: Univalent foundations of mathematics"; although this could refer to either usage, since the book only discusses HoTT as a mathematical foundation.[2]
More recently, Voevodsky has tried to distance himself from certain perspectives on homotopy type theory that he disagrees with, and to reserve the term "univalent foundations" for those that involve his own research, such as the UniMath library of formalized mathematics.[5][13] It remains to be seen whether this usage will become dominant.[7][8][9]

VV in his edit of 17:55, 12 February 2015 - with no edit summary note - completely rewrote this section as follows:

Univalent foundations
The phrase "univalent foundations" was introduced by Vladimir Voevodsky to refer to his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant.[10]
When Voevodsky presented his work to the community of other researchers working on homotopy type theory there was, along with much interest in the mathematical constructions that he invented, a common unwillingness and hesitation to support the idea that this can indeed be a new foundation of mathematics. The phrase "homotopy type theory" was chosen instead to emphasize that those working on the subject do not challenge the accepted foundations of mathematics but only develop a new field inside the existing paradigm. The definition of the homotopy type theory given in the HoTT book emphasizes this point of view. Over the last few years as it was becoming clear that the claim that Voevodsky was making has a substance, the phrase "homotopy type theory" started to be used more and more often interchangeably with the univalent foundations as a name for a new approach to foundations of mathematics.
One of the problems that arose after the special year was the over-emphasis in the presentations related to HoTT on the so called "synthetic homotopy theory". This over-emphasis was creating the opinion among mathematicians less familiar with the details of the subject that the the main uses of HoTT were in formalization of homotopy theory through the use of synthetic constructs such as higher inductive types distracting the attention from the fact that it provided the best available environment for the formalization of the usual set-theoretic mathematics in type theories such as MLTT and CIC. Voevodsky, in particular in his Bernays lectures,[7][8][9] was trying to correct this misconception by emphasizing the possibilities that the univalent foundations presented for the formalization of the ordinary set-theoretic mathematics, including classical mathematics.

This new version by VV contained no citations other than for his own Bernays lectures and also a blog titled 'Homotopy Type Theory' which then has a subtitle 'Homotopy Type Theory and Univalent Foundations'. Moreover, the page cited says that UF is "...based on the homotopical interpretation of type theory." So even in his own citations VV demonstrates how intimately related the two terms are. Notice also that VV in his edit said, "...the phrase 'homotopy type theory' started to be used more and more often interchangeably with the univalent foundations as a name for a new approach to foundations of mathematics." So is VV arguing against a merge of the two article, or for it?

This edit was immediately reverted by Michael Shulman on 18:28, 12 February 2015 with the comment “That's totally contrary to my memory of events, and also (it seems to me) to the text of the book; it would need to be backed up by citations.”

Sources of this material

Many of these arguments have simply been condensed and rearranged from material already in WP. See the following pages:

References

  1. ^ IAS School of Mathematics: Univalent Foundations of Mathematics
  2. ^ a b c Homotopy Type Theory: Univalent Foundations of Mathematics
  3. ^ Awodey, Steve (2014). "Structuralism, Invariance, and Univalence" (PDF). Philosophia Mathematica. 22 (1). Oxford University Press. doi:10.1093/philmat/nkt030. ISSN 0031-8019. Retrieved 13 December 2014.
  4. ^ HoTT page at nLab
  5. ^ a b c UniMath
  6. ^ a b Foundations
  7. ^ a b c Bernays lecture 1
  8. ^ a b c Bernays lecture 2
  9. ^ a b c Bernays lecture 3
  10. ^ a b Type Theory and Univalent Foundations
  11. ^ See especially the Introduction to Homotopy Type Theory: Univalent Foundations of Mathematics
  12. ^ Homotopy Type Theory: References
  13. ^ Voevodski 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).
Retrieved from "https://en.wikipedia.org/w/index.php?title=User:Foobarnix/Article_builder_1&oldid=685771402"