Theorem SSet.Truncated.Edge.CompStruct.comp_unique

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.Edge.CompStruct.comp_uniqueView on Github →