Eric Finster: Towards an Opetopic Type Theory

The realization that dependent type theory has a higher categorical interpretation where types are coherent higher groupoids has been a
major development in the field.  However, while internally types exhibit coherent structure provided by their identity types, type theory itself still lacks any mechanism for describing more general coherent objects.  In particular, it has no means of describing higher equivalence relations (i.e. internal higher groupoid objects) or coherent diagrams of types (functors into the universe). Much work has focused on the search for reasonable internal notion of simplicial types to remedy this problem, but to date no simple solution has been found.

In this talk, motivated by recent progress in formalizing the Baez-Dolan opetopic definition of higher categories in type theory, I will present an alternative approach to coherence based on opetopes. The theory of opetopes is based on the theory of polynomial functors, also known as as W-types or containers in the type theory literature, and thus fits naturally with concepts already familiar from logic and computer science.  I will sketch a type theory extended with syntax for manipulating opetopic expressions a explain how this leads to a  quite general logical theory of coherence.