Sanjeevi Krishnan
The Ohio State University
Title
(Homotopy) Type theory for the working mathematician
Abstract
We introduce type theory accessible to the general mathematician unfamiliar with type-theoretic terminology and notation. The goal of the talk is to prepare the audience with some recent variants of Martin-Lof dependent type theory and its homotopical extensions for two other planned upcoming events (the geometric group theory seminar on November 20 and the departmental colloquium on December 4). Some of the questions that will be answered are: In what sense can propositions be interpreted as (data) types and proofs be interpreted as computer programs having prescribed input and output (data) types? In what further sense can propositions be generalized to the data of fibre bundles, term substitutions be interpretable as parallel transport between fibres, and proofs interpretable as fibre equivalences or abstractly as paths in an associated classifying space? How can this interpretation be used to get a computer to make hitherto difficult computations in topology and, perhaps one day, geometry?