An Enriched Approach to the Strictification of (, 1) -Categories

We define a functor which takes in an (, 1) -category and outputs an (ω, 1) -category, the natural maximally "strict" version of an (, 1) -category. We do this by modeling (, 1) -categories as categories enriched in -groupoids, and then "locally strictifying" (applying the strictification of -groupoids to each hom space) to obtain a category enriched in ω-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 ω-groupoids, which is equivalently an (ω, 1) -category. We conjecture that this functor is conservative, and prove this for two dual special cases: 2-truncated and 2-connected (, 1) -categories. Along the way, we construct a sort of "incoherent walking (ω, 1) -equivalence, " which gives a simpler description of the coherent path lifting condition for fibrations of (ω, 1) -categories, only involving cells of dimension 3.