You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Oct 04 2021 at 15:54):This Thursday (the 7th) at 15:00 UTC (two hours earlier than normal — if you've synced your calendars from researchseminars.org, this changed time might not have shown up yet)
Tim Hosgood (Oct 04 2021 at 15:54):Anders Mortberg: Cubical Methods in Homotopy Type Theory and Univalent Foundations
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.
Tim Hosgood (Oct 04 2021 at 15:54):YouTube: https://youtu.be/p9ANNglWMvc
Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=Znh3UlUrek41T3RLQXJVRVNkM3Ewdz09
Tim Hosgood (Oct 07 2021 at 13:32):starting in an hour and a half!
Jacques Carette (Oct 10 2021 at 13:28):Could we get the slides?
Tim Hosgood (Oct 10 2021 at 20:17):they're up on the colloquium webpage :-)
https://topos.site/topos-colloquium/slides/2021-10-07.pdf