Simplicial (homotopy coherent) nerve

Stream: Infinity-Cosmos

[Dagur Asgeirsson]

I have defined the simplicial nerve (also called homotopy coherent nerve) of a simplicial category in mathlib PR #19837.

This is not directly related to this project right now, but might be useful later.

It will definitely be useful to construct explicit examples of infinity categories, for example Lurie defines the $\infty$-category of anima (spaces) as the simplicial nerve of the simplicial category of Kan complexes. This is the most explicit way to do it and immediately gives the functor from honest topological spaces to anima.

I have not proved anything useful about this construction yet, but there is a list of projects in the module docstring

[Emily Riehl]

Congrats @Dagur Asgeirsson. This looks really great.