An Enriched Approach to the Strictification of $(\mathrm{\infty },1)$-Categories

We define a functor which takes in an $(\mathrm{\infty },1)$-category and outputs an $(\omega ,1)$-category, the natural maximally “strict” version of an $(\mathrm{\infty },1)$-category. We do this by modeling $(\mathrm{\infty },1)$-categories as categories enriched in $\mathrm{\infty }$-groupoids, and then “locally strictifying” (applying the strictification of $\mathrm{\infty }$-groupoids to each hom space) to obtain a category enriched in $\omega$-groupoids with respect to the Gray tensor product, followed by “globally strictifying” (strictifying the enrichment from the Gray tensor product to the cartesian product) to obtain a category cartesian-enriched in $\omega$-groupoids, which is equivalently an $(\omega ,1)$-category. We conjecture that this functor is conservative, and prove this for two dual special cases: $2$-truncated and $2$-connected $(\mathrm{\infty },1)$-categories. Along the way, we construct a sort of “incoherent walking $(\omega ,1)$-equivalence,” which gives a simpler description of the coherent path lifting condition for fibrations of $(\omega ,1)$-categories, only involving cells of dimension $\le 3$.