Commit 2024-11-14 20:28 76f52eb2

feat(AlgebraicTopology/SimplicialSet): paths and the strict segal condition (#18499) A path in a simplicial set X of length n is a directed path comprised of n 1-simplices. An n-simplex has a maximal path, the spine of the simplex, which is a path of length n. A simplicial set X satisfies the StrictSegal condition if for all n, the map X.spine n : X _[n] → X.Path n is a bijection. Examples of StrictSegal simplicial sets are given by nerves of categories. Future work will show these are the only examples: that a StrictSegal simplicial set is isomorphic to the nerve of its homotopy category. Co-Authored-By: Mario Carneiro and Joël Riou