Delooping in homotopy type theory

Question

In algebraic topology, it is a theorem of Stasheff that every A-$\infty$ space has the homotopy type of a loop space.

Question: Is this true in homotopy type theory?

Let me be a little more precise. Let $X$ be a type. Assume that we have $e : X$ and $ m : X \times X \to X$ together with the following data:

• $ a : \prod_{x,y,z:X} m(x,m(y,z)) = m(m(x,y),z) $
• $l : \prod_{x : X} m(e,x) = x$
• $r : \prod_{x : X} m(x,e) = x$

Can we find a type $Y$ such that $ X $ is equivalent to $ \Omega Y$?

EDIT: Charles and Anton are exactly right. $X$ as defined above should behave like an $A_1$ space. The reason that I got confused is as follows: If $f : X \to Y$ is an equivalence in the sense of HTT then we can transport $m,a,l,r$ over to $Y$. This follow from the univalence axiom and is described in some detail in the univalent foundations book. If $f : X \to Y $ is a homotopy equivalence of topological spaces, then you cannot transport an $A_1$ structure from $X$ to $Y$ along $f$. All you know is that $Y$ is an $A_{\infty}$ space. Is there an explanation for this discrepancy?

Answer 1

The definition you gave is not of an $A_\infty$-space, but just of $A_1$-space. As Charles noted, these two classes of spaces are very different in general. For example, there are also higher isomorphisms similar to the ones in MacLane's pentagon identity for monoidal categories, and relations between them, ad infinitum. There is no a priori reason for these higher coherence morphisms to exist. You also need to state that $X$ is grouplike, but that one is simple: just give a map $\iota : X\to X$ such that $m(x,\iota(x)) = m(\iota(x), x) =x$.

$A_1$ and $A_\infty$ structures on $X$ are the same if $X$ is discrete. In this case the delooping was constructed in the paper "Eilenberg-MacLane spaces in homotopy type theory" of Daniel R. Licata and Eric Finster. Specifically, they prove that for any discrete $A_1$-space $G$ there exist an inductively defined space $BG$, such that $BG$ is 0-connected, 1-truncated and $\Omega BG = G$ as groups. In fact, we can get $BG$ as a 1-truncation of the space $(\Sigma G)^\prime$. Here $(\Sigma G)^\prime$ is the suspension of $G$ with extra glued up 2-cells corresponding to the identities $a_{x,y,z}: (xy)z=x(yz)$. If $G$ is abelian, then we can also define higher Eilenberg--MacLane spaces as $$K(G,n) := \Vert \Sigma^{n-1} K(G,n) \Vert_n$$

Here $\Sigma$ is the reduced suspension and $\Vert\cdot\Vert_n$ is the n-truncation of homotopy types.

Similarly, there should be a delooping of any $A_\infty$-space, constructed as a similar higher inductive type with generators of all orders, but the fundamental open problem of HoTT is to define what is an $A_\infty$-space, since it involves an infinite number of seemingly different relations.