Voevodsky’s univalent foundations and homotopy type theory comprise a new and radical approach to the foundations of mathematics in which the structural properties of equality are extended to every possible form of equivalence and symmetry, leading to an expanded universe of discourse in which ordinary sets and algebraic structures exist harmoniously alongside infinite-dimensional spaces. In this talk, I will expose the basic grammar and vocabulary of the new univalent foundations — and explain how they shed light on basic problems in theoretical computer science and the specification of computer programs.
Link to join virtually: https://cam-ac-uk.zoom.us/j/81322468305
This talk is being recorded.