I read on the [nLab][1] that in "Pursuing stacks" Grothendieck made several interesting conjectures, some of which have been proved since then.  For example, as David Roberts wrote in answer to [this question](https://mathoverflow.net/questions/61781/what-is-the-homotopy-theory-of-categories/61783#61783),

>  Grothendieck conjectured, and Cisinski proved, that the class of weak equivalences in the Thomason model structure was the smallest basic localizer.

I am interesting in knowing what other conjectures made in PS have turned out to be true, or  other "ideas" that have been successfully realized/formalized.  Ideally it would be nice to include references to the relevant papers.

  [1]: https://ncatlab.org/nlab/show/Pursuing+Stacks