Higher categories from type theories

Abstract

This thesis continues the programme of providing a higher-categorical analysis of the treatment of equality in Martin-Lof dependent type theory. In particular, we construct for various type theories a classifying weak ω-category, with objects and 1-cells as in the standard classifying category, and higher cells being open terms of identity types between these. Weak ω-category structures (in the sense of Batanin/Leinster) on these are given by operads of syntactically definable composition laws.