Skip to main content

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 ( )
2. The Boardman-Vogt resolution of operads in monoidal model categories ( )