feat(AlgebraicTopology/SimplicialSet): refactor StrictSegal via SSet.Truncated

[gio256]

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 first for truncated simplicial sets. The respective constructions on SSet are then defined in terms of these canonical truncated definitions.

---

• depends on: feat(AlgebraicTopology): truncated simplicial notations #20688
• depends on: feat(AlgebraicTopology): delaborators for truncated simplicial notations #20719

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(AlgebraicTopology): truncated simplicial notations #20688
• feat(AlgebraicTopology): delaborators for truncated simplicial notations #20719
  By Dependent Issues (🤖). Happy coding!

[emilyriehl]

If I'm reading this correct, StrictSegal X is the structure of an (n + 1)-StrictSegal structure on the (n+1)-truncation of X for all n. If this is right, this feels very redundant because we're specifying explicit equivalences for each map X.spine m : X _[m]→Path X m infinitely many times (for each n so that m ≤ n + 1).

The code you've deleted specifies each equivalence exactly once. Is there a way to do this while re-using the truncated versions of the code?

[gio256]

This also surprises me a bit. One thought is that this redundancy is removed if Truncated.StrictSegal is defined such that an n + 1-truncated simplicial set X is Truncated.StrictSegal when its n + 1-simplices are uniquely determined by their spine (rather than its m-simplices for all m ≤ n + 1). But, this still strikes me as the wrong definition for the truncated case.

Relatedly, I was surprised that I never needed any sort of proof that the StrictSegal data at each truncation level agreed with the data from the lower truncation levels. I will give this all some more thought.

[emilyriehl]

Yes, I agree that's the wrong definition in the truncated case. Though perhaps Truncated.StrictSegal could be defined such that an n + 1-truncated simplicial set X is Truncated.StrictSegal when its n + 1-simplices are uniquely determined by their spine AND its further n-truncation is Truncated.StrictSegal (inductively now in n).

[emilyriehl]

But let's let @joelriou weigh in.