Commit 2025-12-02 14:25 30dfca1e
View on Github →feat(AlgebraicTopology/Quasicategory): define the homotopy category of a 2-truncated quasicategory (#31630)
The homotopy category HomotopyCategory₂ A of a 2-truncated quasicategory A has:
- objects given by the vertices of
A - morphisms given by (left) homotopy classes of edges between two vertices. From: https://github.com/emilyriehl/infinity-cosmos