Theorems · Inductive type · category theory
CategoryTheory.SmallObject.SuccStruct
(C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)A successor structure on a category consists of the
data of an object succ X for any X : C, a map toSucc X : X ⟶ succ X
(which does not need to be natural), and a zeroth object X₀.
- Cited by
- 54 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
Cited by95
Results whose statement or proof uses this declaration.
- CategoryTheory.SmallObject.SuccStruct.Iterationstatement · cited by 29
- CategoryTheory.SmallObject.SuccStruct.Iteration.Fstatement and proof · cited by 23
- CategoryTheory.SmallObject.SuccStruct.propstatement and proof · cited by 18
- CategoryTheory.SmallObject.SuccStruct.succstatement and proof · cited by 15
- CategoryTheory.SmallObject.SuccStruct.toSuccArrowstatement and proof · cited by 14
- CategoryTheory.SmallObject.SuccStruct.iterationFunctorstatement and proof · cited by 12
- CategoryTheory.SmallObject.SuccStruct.X₀statement and proof · cited by 10
- CategoryTheory.SmallObject.SuccStruct.toSuccstatement and proof · cited by 10
- CategoryTheory.SmallObject.SuccStruct.Iteration.mapObjstatement and proof · cited by 7
- CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystemstatement and proof · cited by 5
- CategoryTheory.SmallObject.SuccStruct.Iteration.congr_objstatement and proof · cited by 5
- CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIterationstatement and proof · cited by 5