Def SSet.HomotopyCategory.objEquiv

Modification history

2026-08-19 11:50
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
feat(AlgebraicTopology/SimplicialSet): induction principle for morphisms of the homotopy category of a simplicial set (#42673)
Added SSet.HomotopyCategory.objEquivView on Github →