Theorems · Definition · category theory
CategoryTheory.MorphismProperty.identities
(C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty CThe property of morphisms that is satisfied by 𝟙 X for any X.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
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.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.CategoryStruct.idproof · cited by 6,235
- CategoryTheory.MorphismPropertystatement · cited by 2,179
- CategoryTheory.MorphismProperty.ofHomsproof · cited by 30
Cited by18
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.ReedyStructure.lt₁statement · cited by 2
- HomotopicalAlgebra.ReedyStructure.lt₂statement · cited by 2
- HomotopicalAlgebra.ReedyStructure.prop₁_of_degHom_eq_deg_rightproof · cited by 2
- HomotopicalAlgebra.ReedyStructure.mk.noConfusionstatement and proof · cited by 1
- HomotopicalAlgebra.ReedyStructure.identities_of_prop₁_of_eqstatement and proof · cited by 1
- HomotopicalAlgebra.ReedyStructure.identities_of_prop₂_of_eqstatement and proof · cited by 1
- HomotopicalAlgebra.ReedyStructure.le₁proof · cited by 1
- HomotopicalAlgebra.ReedyStructure.le₂proof · cited by 1
- HomotopicalAlgebra.ReedyStructure.prop₂_of_degHom_eq_deg_leftproof · cited by 1
- HomotopicalAlgebra.ReedyStructure.mk.injstatement and proof · cited by 1
- HomotopicalAlgebra.ReedyStructure.mk.sizeOf_specstatement and proof · cited by 0
- HomotopicalAlgebra.ReedyStructure.casesOnstatement and proof · cited by 0