Theorems · Definition · algebraic topology
SSet.Truncated.HomotopyCategory.mk
{V : SSet.Truncated 2} →
V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }) → V.HomotopyCategoryConstructor for objects of the homotopy category of a 2-truncated simplicial set.
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Oppositestatement · cited by 8,081
- SimplexCategorystatement · cited by 2,204
- SimplexCategory.lenstatement · cited by 542
- SimplexCategory.Truncatedstatement · cited by 236
- SSet.Truncatedstatement and proof · cited by 214
- SSet.Truncated.HomotopyCategorystatement · cited by 54
- CategoryTheory.Cat.FreeRefl.mkproof · cited by 17
- SSet.Truncated.HomotopyCategory.quotientFunctorproof · cited by 5
Cited by49
Results whose statement or proof uses this declaration.
- SSet.Truncated.HomotopyCategory.homMkstatement · cited by 24
- SSet.Truncated.HomotopyCategory.mkNatIsostatement and proof · cited by 5
- SSet.Truncated.HomotopyCategory.homToNerveMkproof · cited by 5
- SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIsoproof · cited by 3
- SSet.Truncated.HomotopyCategory.homMk_comp_homMkstatement · cited by 3
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIsoproof · cited by 3
- SSet.Truncated.HomotopyCategory.mkNatTransstatement and proof · cited by 2
- SSet.Truncated.HomotopyCategory.mk_surjectivestatement · cited by 2
- SSet.Truncated.HomotopyCategory.congr_arrowMk_homMkstatement · cited by 1
- SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMkstatement · cited by 1
- SSet.Truncated.HomotopyCategory.functor_extstatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.homToNerveMk_app_edgestatement · cited by 1