Prove that in HoTT if types $A$ and $B$ are connected and $\Omega A = \Omega B$, then $A = B$

Question

In Homotopy Type Theory, suppose that $A, B : \mathcal{U}$, and $a_0 : A$ and $b_0 : B$.

Further, suppose that A and B are connected, so we have $\prod_{a:A}||a_0 = a||$ and likewise for B.

Finally suppose that $(a_0 = a_0) = (b_0 = b_0)$.

Is it possible from these conditions to prove that $A=B$? From my understanding of types as $\infty-$groupoids, it seems that it should be possible.

Answer 1

Here is a counterexample:

Consider the Eilenberg-Mac Lane spaces $K(\mathbb{Z}_2\times\mathbb{Z}_2,1)$ and $K(\mathbb{Z}_4,1)$. Those are non-equivalent connected types with equivalent (hence equal) loop spaces. The issue here is that the equivalence of loop spaces is just an equivalence between two 4-element types, but not a group isomorphism.