# 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.

References

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
)