Anders Mortberg: "Cubical Methods in Homotopy Type Theory and Univalent Foundations"

7th of October, 2021. Part of the Topos Institute Colloquium.
-----
Abstract: One of the aims of Homotopy Type Theory and Univalent Foundations (HoTT/UF) is to provide a practical foundation for computer formalization of mathematics by building on deep connections between type theory, homotopy theory and (higher) category theory. Some of the key inventions of HoTT/UF include Voevodsky's univalence axiom relating equality and equivalence of types, the internal stratification of types by the complexity of their equality, as well as higher inductive types which allow synthetic reasoning about spaces in type theory. In order to provide computational support for these notions various cubical type theories have been invented. In particular, the Agda proof assistant now has a cubical mode which makes it possible to work and compute directly with the concepts of HoTT/UF. In the talk I will discuss some of the mathematical ideas which motivate these developments, as well as show examples of how computer mechanization of mathematics looks like in Cubical Agda. I will not assume expert knowledge of HoTT/UF and key concepts will be introduced throughout the talk.

[@jlp7185]

nice talk! I appreciate the 10,000-ft view on the subject (which is harder to get from some of the standard sources.)

[@JosiahWarren]

Nicely done. I like the agda notation. Is more minimal that Martin loff notation.

[@3a146]

Well, maybe we can pull a mathematiican as our runtime.

[@3a146]

Or maybe use blockchain to let mathematicians inject postulations and cancel injected when necessary. I believe it's the original idea of Brouwer. Voevodsky did not care about computability that much. I believe the reason why he liked constructive style type theory was because of axiomatic freedom. Mathematics is inductive at the end of the day, and the problem is what if we include a wrong thing? I guess Voevodsky's answer is to explicitly let computer keep track of axioms assumed, if something ever goes wrong, we might just remove the assumption, and fill the hole. Without axioms, it would just be too hard to handle infinities, which are essential to physicists to make phenomenological judgements. Just like mathematicians always hide complexities in symbolic abstractions, physicists tend to hide paradoxes in continuous errors. A real mathematical engine should not only represent already known formal structures, but also admit weaker structure with inductive conjectures such that we may extend the judgements using already known right things to maximize the possibility to detect flaws in all sciences as early as possibly. Many so called scientific domains have already lost clue of what their judgements are about, and the only left truth is the bandwagon waste of limited scientific fundings.

[@StevenKane1983]

Candidly, this talk is boring. He makes his topic of research sound bland when in fact it's one of the more exciting things going on in the modern world of research computer science.

[@noninvasive_rectal_probe8990]

Not much interesting here. I wonder if you could instead present the topic with some visual aid.
To know about how typecheker works by giving some overview on some terms. More info on internals, Anders!

[@MarieAmeliaFreyaAster]

nice name

[@JonathanSterling]

I think you should consider that the author of this talk will see these comments... You should be ashamed. By the way, it probably would not be appropriate to speak of technical details of type checkers and code at the Topos Institute's colloquium. One thing people learn quite quickly with academic communication, which perhaps could be learnt by youtube commenters, is to consider your audience.

[@noninvasive_rectal_probe8990]

@@JonathanSterling drop this elitist tone, stein. His presentation about compex topic was at least vacuos and at most barren, and you better spend some time thinking about resons by which those proffersors are guide so they publish these recordings in a public domain. Which is - here is a hint to simplify you your coming mental struggle - to expose the topic to wider audience.
Regarding the substantial matter, I believe that implementation of these ideas are whats most valuable here, cus working code worth more than thousands of utterances of any abstract nonesense, and I hope that Anders or other two people who made the thing will bother to give general overview of how this all works rather than saying again what they have said dozens of times. There is alternative route to be taken, other than mathspeak, which I hope is the one that will be.