COHERENCE IN CATEGORIES AND IN DEPENDENT TYPE THEORY

Expositor: Pierre Louis Curien
Institución: DR CNRS, Laboratoire PPS, University Paris 7, Francia.

Jueves 27 de marzo de 2014.
16:00-17:00.

Resumen:We shall recall briefly Mac Lane’s coherence theorem for monoidal categories, and discuss two quite different proofs of it. We shall then explain how similar coherence issues arise in dependent type theory and how they can be solved using similar techniques. To be as self-contained as possible, we shall provide a brief introduction to type theory, hinting even more briefly at recent developments going on under the name of Homotopy Type Theory.