Type theory and higher categories

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.