Upon further reflection, perhaps Lurie's original treatment of Straightening-Unstraightening can be viewed as a (partial) formalisation of this theorem. After all, Lurie first provides a Quillen equivalence over simplices (using the mapping simplex), and then uses, that any quasi-category is generated by its simplices.

@DylanWilson Thank you! This looks great

@DenisNardin These notes by Yonatan Harpaz might give you some ideas on how to balance between "foundations" and "applications" math.univ-paris13.fr/~harpaz/lecture_notes.pdf