Grothendieck's homotopy hypothesis for infinity-groupoids

Let $\mathsf{Hot}$ be the homotopy category of topological spaces, let $C$ be a coherator, and let $\overline{\Pi_\infty}$ be the functor induced by the fundamental infinity-groupoid functor from topological spaces to Grothendieck infinity-groupoids of type $C$, after localization at weak equivalences.

Grothendieck's conjecture. The functor $\overline{\Pi_\infty}$ is an equivalence of categories.

This is Grothendieck's homotopy hypothesis, asserting that Grothendieck infinity-groupoids provide an algebraic model for homotopy types. The precise formulation depends on a coherator and the corresponding notion of weak equivalence; the source presents the assertion as a conjecture.