Univalence from a computer science point-of-view

Dan Licata
Wesleyan University
September 14, 2018
Abstract: One formal system for Voevodsky's univalent foundations is Martin-Löf's type theory. This type theory is the basis of proof assistants, such as Agda, Coq, and NuPRL, that are used not only for the formalization of mathematics, but in computer science for verification of programs, systems, and programming language designs and implementations. These applications rely on the fact that constructions in type theory can be interpreted constructively as programs.