Errol Yuksel: Coherence in monoidal categories via type theory

Abstract

Monoidal categories are a categorical notion of monoids, where the associativity and unit laws hold up to isomorphism. Introducing isomorphisms leads to some subtle coherence issues that Mac Lane solved by adding minimal conditions such as his famous pentagon diagram. 

In this talk, we will define monoidal categories and give an alternative proof of Mac Lane's coherence theorem. This proof, due to Beylin and Dybjer, is type-theoretical in nature and relies on the notion of normalization. If time permits, we will also reframe said proof into a more general setting.