Emily Riehl on Univalent Foundations

There's something sane and healthy-sounding about this whole thing!

See Clive Newstead's book An Infinite Descent into Pure Mathematics and Egbert Rijke's Introduction to Homotopy Type Theory course at CMU https://github.com/EgbertRijke/HoTT-Intro. Unfortunately the last lines of Emily's slides aren't always visible on the video, see e.g. 35:54.

At 41:24 on the difference between the existential and universal quantifiers and the constructive sum and product types, see Set Theory for Computer Science by Glynn Winskel and Fraenkel–Mostowski models revisited by Jindrich Zapletal.

1:01:20 On Guillaume Brunerie's theorem (There exists a natural number n such that π4(S3)≃ℤ/nℤ.), see his PhD thesis: On the homotopy groups of spheres in homotopy type theory. And if  you wonder what it all means, like I do, see the Wikipedia article on Homotopy groups of spheres.

For more on Cubical Agda, see Cubical agda: a dependently typed programming language with univalence and higher inductive types.

Subscribe to Fields Institute.

The X Files, Series XVII:

From the first three pages of the Introduction in S.W.P. Steen's Mathematical Logic:

He identifies two means of defining a metalanguage. The first is the traditional method of using a less well-defined language to define a more precise one, the second is by enumerating the sentences and striking out all those which are not well-formed. This process, he says, would be "lengthy and boring in the extreme" but if we had a finite abstract description of that syntax then we could make a machine test each sequence and strike out all those which are ill-formed. That is effectively what a parsing program does.

The Internet Archive has this book, but for the last few weeks it has not been available in the UK.

See Vladimir Voevodsky's Heidelberg Laureate Forum Talk from September 2016:

From September 2016.

"... it came out, as a result of practical work on formalization we just discovered that the law of excluded middle and axiom of choice can be avoided in the univalent foundations much more successfully than they can be avoided in set theory, so things which can not be done without them in set theory can be done without them in the univalent foundations, so then there was this understanding that the classical mathematics appears as a subset of this new constructive mathematics. That is actually kind of an easy easy thing to see, but it's important to emphasize that one obtains the view of mathematics as constructive and then the classical mathematics as a subset of this constructive mathematics, a very important subset, and it's kind of a retract: it's not only a subset but it's it's a retract, but it's still a subset" And he  goes on: "The understanding that the MLTT extended with the UA is an imperfect formalization system for this constructive mathematics and that it should be possible to integrate the UA into the MLTT obtaining a new type theory with better computational properties." And so it turned out, see Emily Riehl's final comment about a constructive proof found in a matter of seconds using Cubical Type Theory.

Slides https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2016_09_22_HLF_Heidelberg.pdf

Subscribe to Heidelberg Laureate Forum.