Theorem SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk

Modification history

2025-12-02 14:25
Mathlib/AlgebraicTopology/Quasicategory/TwoTruncated.lean
feat(AlgebraicTopology/Quasicategory): define the homotopy category of a 2-truncated quasicategory (#31630) …
Added SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMkView on Github →