Def SSet.Homotopy

Modification history

2026-03-27 09:21
Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean
feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by a homotopy (#33683) …
Added SSet.HomotopyView on Github →