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