Commit 2024-11-25 11:42 2fa86db9

feat(AlgebraicTopology): StrictSegal simplicial sets are quasicategories (#19270) We prove that any simplicial set satisfying the StrictSegal condition introduced in #18499 is a quasicategory. This implies that the nerve of a category is a quasicategory. We construct a solution to the lifting problem against hornInclusion n i as a spineToSimplex of the path in the image of the spine of the standard simplex. To prove that this extension restricts to the appropriate map on the horn, we apply spineInjective, reducing the question of equality between two n-simplices in X to that of equality between the paths along their spines. The remainder of the proof is a straightforward application of basic properties relating spines of simplices to their faces. Co-Authored-By: Johan Commelin and Emily Riehl