# Delooping in homotopy type theory

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?

-
As you've stated this, it is not even true in the simplicial set model of HoTT: (grouplike) associative $H$-spaces are not in general deloopable. –  Charles Rezk Aug 10 at 17:11
@CharlesRezk: I am confused now. In the sset model, shouldn't (X,m,a,l,r) be an A-infinity space? You can deloop A-infinity spaces right? –  Daniel Barter Aug 10 at 17:29
An A-infinity space is given by an infinite list of data, encoding higher homotopies. And remember that "f = g" means "space of homotopies from f to g" –  Charles Rezk Aug 10 at 17:54
I don't understand what you are saying in your edit. You can certainly transport $A_1$-structures along homotopy equivalences. –  Charles Rezk Aug 21 at 19:57
$A_1$-spaces are classically called H-spaces. It is a theorem that H-spaces are precisely the retractions of $A_\infty$-spaces. Retractions can change your space pretty wildly. For example, a retraction of a finite CW-complex can be not equivalent to a finite CW-complex (see Wall finiteness obstruction). It would be more surprising if $A_1$ and $A_\infty$ happened to coincide. –  Anton Fetisov Aug 21 at 20:46

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.
I agree with you, of course. A major winning point for HoTT is that "$\infty$-groupoid" is just "type", and that equivalence requires no higher-dimensional conditions (which one might expect). So we do have examples where an infinite amount of higher-dimensional structure is dealt with without explicit reference to it. –  Andrej Bauer Aug 11 at 17:27