Theorems · Definition · category theory

CategoryTheory.SmallObject.SuccStruct.iterationFunctor

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

Given Φ : SuccStruct C and a well-ordered type J, this is the functor J ⥤ C which gives the iterations of Φ indexed by J.

Defined in

Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Cited by

12 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryLinearOrderOrderBotSuccOrderWellFoundedLTCategoryTheory.Limits.HasIterationOfShape