refactor(AlgebraicTopology/SimplicialSet): 0-truncated paths

[gio256]

An experimental alternative to #20668.

The most notable difference here is that the vertices of a path in an n-truncated simplicial set X live in the further 0-truncation of X, rather than the 1-truncation. The arrows are then 1-simplices in the further 1-truncation of X whose sources and targets can be identified with the respective vertices. This allows us to consider paths in 0-truncated simplicial sets (without arrows) as well as in n + 1-truncated simplicial sets (with arrows).

The diff is a mashup of several different PRs at this point, so the intrepid reviewer may prefer to just read through Path.lean.

---

[github-actions]

PR summary 53dc574c96

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplexCategory	818	819	+1 (+0.12%)
Mathlib.AlgebraicTopology.SimplicialObject.Basic	833	834	+1 (+0.12%)
Mathlib.AlgebraicTopology.SimplicialSet.Basic	834	835	+1 (+0.12%)
Mathlib.AlgebraicTopology.SimplicialSet.Path	843	844	+1 (+0.12%)
Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal	849	850	+1 (+0.12%)
Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal	851	852	+1 (+0.12%)
Mathlib.AlgebraicTopology.Quasicategory.StrictSegal	852	853	+1 (+0.12%)
Mathlib.AlgebraicTopology.Quasicategory.Nerve	853	854	+1 (+0.12%)
Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat	857	858	+1 (+0.12%)

Import changes for all files

Files

Import difference

50 files Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplexCategory Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicTopology.SimplicialObject.Split Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution

1

---

Declarations diff

+ CategoryTheory.Nerve.strictSegal
+ Hom.tr
+ Hom.tr_comp
+ Meta.subscript
+ Path₀
+ Path₁
+ StrictSegalAux.of_zero
+ arrow_rec
+ ext
+ ext₀
+ ext₁
+ hasColimits
+ hasLimits
+ hom_ext
+ incl
+ incl_comp_inclusion
+ instance (C : Type u) [Category.{v} C] :
+ instance : Coe (((truncation 1).obj X).Path 0) (Path X 0)
+ instance {X : SSet.Truncated.{u} n} {m : ℕ} :
+ largeCategory
+ mk_arrow
+ mk_vertex
+ on
+ spineEquiv_coe_fn
+ spineEquiv_symm_coe_fn
+ spineToDiagonal_def
+ spine_arrow'
+ trunc_eq
+ trunc_self
+ trunc_spine
+ uliftFunctor
++ arrow
++ arrow_src
++ arrow_tgt
++ map_arrow
++ map_vertex
++ mk
++ spineToSimplex
++ spineToSimplex_spine
++ spineToSimplex_spine_apply
++ spine_arrow
++ spine_spineToSimplex
++ spine_spineToSimplex_apply
++ spine_vertex
++ vertex
+++ delabMkNotation
+++ ext'
+++ truncation_comp_trunc
++++ interval
++++ map
++++ trunc
++- Path
++- map_interval
++- spineInjective
++- spine_map_vertex
+-+ StrictSegal
+-+ spine
+-+ spineEquiv
+-+ spineToDiagonal
+-+ spineToSimplex_arrow
+-+ spineToSimplex_vertex
- Path.ext'
- Path.interval
- Path.map
- Truncated.hasColimits
- Truncated.hasLimits
- Truncated.hom_ext
- Truncated.largeCategory
- Truncated.uliftFunctor
- horn.spineId_map_hornInclusion
- spineToSimplex_map
- strictSegal
-++ spineToSimplex_edge
-++ spineToSimplex_interval
-++ spine_δ_arrow_eq
-++ spine_δ_arrow_gt
-++ spine_δ_arrow_lt
-++ spine_δ_vertex_ge
-++ spine_δ_vertex_lt

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
1418	1	erw

Current commit 53dc574c96
Reference commit 773fd70b27

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).