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$?

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?

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 \to 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$?

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$?