# Vladimir Voevodsky

## Type Systems

## Type Systems

## Type Systems and Proof Assistant

## Type Systems

## Overview of Univalent Foundations

(Continued from September 26, 2012)

## Computer Science and Homotopy Theory

## Univalent Foundations of Mathematics

The correspondence between homotopy types and higher categorical analogs of groupoids which was first conjectured by Alexander Grothendieck naturally leads to a view of mathematics where sets are used to parametrize collections of objects without "internal structure" while collections of objects with "internal structure" are parametrized by more general homotopy types. Univalent Foundations are based on the combination of this view with the discovery that it is possible to directly formalize reasoning about homotopy types using Martin-Lof type theories.

## What if Current Foundations of Mathematics are Inconsistent?

This lecture was part of the Institute for Advanced Study’s celebration of its eightieth anniversary, and took place during the events related to the Schools of Mathematics and Natural Sciences.