Commit 2024-11-22 18:29 3d401e0b
View on Github →feat(AlgebraicTopology/SimplicialSet): Add auxiliary ext lemma for paths (#19349) We implement the generalization of the path extensionality lemmas suggested by @joelriou in #19057. Two paths of the same nonzero length can be identified by constructing an identification between each of their arrows. Co-Authored-By: Joël Riou