Abstract

Throughout category theory, it is often the case that objects should be considered up to isomorphism instead of up to equality. In higher dimensional theories, this can be taken a step further by replacing equational laws (such as associativity of composition) by existence of a higher dimensional equivalences. Such theories are called “weak”, and while they are more expressive they become much harder to work with, motivating the search for “semistrict” definitions of higher categories.

I will give a brief history of some of the motivations and results in this area, before explaining our work on using type theories to give semistrict definitions of infinity categories. I will attempt to assume as little knowledge as possible, and rely on examples instead of any technical details.