Hugo Moeneclaey: Monoids up to Coherent Homotopy in Two-Level Type Theory
Time: Wed 2019-03-27 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Lecturer: Hugo Moeneclaey
Abstract : 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.
1. Axiomatic homotopy theory for operads ( arxiv.org/abs/math/0206094 )
2. The Boardman-Vogt resolution of operads in monoidal model categories ( arxiv.org/abs/math/0502155 )