Theorems · Definition · category theory
SimplexCategory.const
(x y : SimplexCategory) → Fin (y.len + 1) → (x ⟶ y)
The constant morphism from ⦋0⦌.
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- SimplexCategorystatement and proof · cited by 2,204
- SimplexCategory.lenstatement and proof · cited by 542
- SimplexCategory.Hom.mkproof · cited by 15
Cited by62
Results whose statement or proof uses this declaration.
- SSet.constproof · cited by 62
- SSet.Truncated.spineproof · cited by 24
- SimplexCategory.const_compstatement · cited by 7
- SimplexCategory.const_eq_idstatement and proof · cited by 6
- CategoryTheory.SimplicialObject.augmentproof · cited by 4
- SSet.StrictSegalCore.concatstatement · cited by 4
- CategoryTheory.CosimplicialObject.augmentproof · cited by 4
- SSet.const_compproof · cited by 4
- SSet.Truncated.spine_vertexstatement · cited by 3
- CategoryTheory.SimplicialObject.equivalenceLeftToRightproof · cited by 3
- SSet.StrictSegal.spineToSimplex_vertexstatement · cited by 3
- CategoryTheory.CosimplicialObject.equivalenceRightToLeftproof · cited by 3