Commit 2025-04-01 11:15 7440afbb

refactor(AlgebraicTopology/SimplicialSet): truncated paths (#20668) We refactor the StrictSegal infrastructure, making two notable changes:

• The StrictSegal class is redefined as a structure, and the class IsStrictSegal X : Prop is added in its place.
• Path, StrictSegal, and related constructions are defined for truncated simplicial sets. A path in a simplicial set X is then defined as a 1-truncated path in the 1-truncation of X.