Theorem SSet.Truncated.HomotopyCategory₂.homMk_surjective

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.HomotopyCategory₂.homMk_surjectiveView on Github →