Theorem 2.1.6 of the Homotopy Type Theory book proves that $\Omega^{2}A$ is always commutative, using a similar argument to the one used for loop spaces in algebraic topology.
Isn't it also the case (left unstated) that one can just use simple path induction to show that this is the case for $\Omega A$ as well? Since $\Omega A :\equiv a =_{A} a$, can't we just show that $p \cdot q = q \cdot p$ by assuming that both $p$ and $q$ are $\mathrm{refl}_{a}$ and using path induction? Doesn't this, much simpler, proof extend to $\Omega^{n}A$ for any $n$? What am I missing?
Ok, I've figured this out. You cannot apply path induction when there are two fixed endpoints. Indeed if you try to actually use the inductor of identity types to create some inhabitant of type $\Pi_{a:A}\Pi_{p,q:a=a} p\cdot q = q \cdot p$ you will fail at the first step of trying to find the correct type family $D : \Pi_{x,y : A} (x =_{A} y) \rightarrow U$ to express your goal. The HoTT book mentions this in 1.12.1.
The reason Lean accepts the proof is because in the non-HoTT version of lean, the only inhabitant of $a=a$ is $\mathrm{refl}_a$.