skip to content

Type theory and higher categories

Presented by: 
Chris Kapulkin
Thursday 6th July 2017 - 13:00 to 13:40
INI Seminar Room 2
Type theory is often referred to as the internal language of higher categories. This covers a range of ideas: results from HoTT can be interpreted in a variety of higher-categorical settings, and conversely, many higher-categorical notions can be expressed and studied in type theory. In this talk, I will report on the progress towards a single master theorem subsuming many of these informal statements.

University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons