Abstract
Supervised by Peter LeFanu Lumsdaine. We present a formalization of monoids up to coherent homotopy in Agda. In order to achieve this we postulate a structure of type theory with two equalities with a notion of fibrant type. Then we build an operad ∞Mon and define monoids up to coherent homotopy as its algebras. We prove that this notion is invariant under equivalences between fibrant types, and that loop spaces are such monoids.
Type
