Phil Math Seminar
William Howard
UIC
The basic type structure underlying Martin-Löf type theory
Abstract: Univalent foundations employs an elaborate type structure whose
main ideas trace back to the basic type structure underlying Martin-Löf
type theory. I'll describe this basic type structure and how it arises
from an attempt to interpret Brouwer's intuitionistic mathematics by means
of a theory of constructions. No knowledge of this field, or of proof
theory, is assumed.
Wednesday March 29, 2017 at 3:00 PM in SEO 427