Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.
The full “100%” version, formalized by Dan, which shows that the relevant map is -connected.
Homotopy limits
Jeremy Avigad, Chris Kapulkin and Peter Lumsdaine arXivCoq code