Theorems · Inductive type · category theory

CategoryTheory.SmallObject.SuccStruct.Iteration

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      CategoryTheory.SmallObject.SuccStruct C →
        [inst_1 : LinearOrder J] →
          [SuccOrder J] →
            [OrderBot J] →
              [CategoryTheory.Limits.HasIterationOfShape J C] → [WellFoundedLT J] → J → Type (max (max u v) w)

The category of jth iterations of a successor structure Φ : SuccStruct C. An object consists of the data of all iterations of Φ for i : J such that i ≤ j (this is the field F). Such objects are equipped with data and properties which characterizes uniquely the iterations on three types of elements: ⊥, successors, limit elements.

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Cited by

29 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

CategoryTheory.CategoryLinearOrderSuccOrderOrderBotCategoryTheory.Limits.HasIterationOfShapeWellFoundedLT