Thursday 11 April 2019, 14:00, LSV library: Monoids up to Coherent Homotopy in Two-Level Type Theory, Hugo Moeneclaey (intern at Stockholm University).

When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2]. Our main results are: (a) Monoids up to coherent homotopy are invariant under homotopy equivalence (b) Loop spaces are monoids up to coherent homotopy. In this talk I will present the classical theory of monoids up to coherent homotopy, and indicates how two-level type theory can be used to formalize it. References 1. Axiomatic homotopy theory for operads (https://arxiv.org/abs/math/0206094) 2. The Boardman-Vogt resolution of operads in monoidal model categories (https://arxiv.org/abs/math/0502155)