Theorems · Definition · category theory

CategoryTheory.ObjectProperty.strictLimitsClosureIter

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C →
      {α : Type t} →
        (J : α → Type u') →
          [(a : α) → CategoryTheory.Category.{v', u'} (J a)] →
            {β : Type w'} →
              [inst_2 : LinearOrder β] → [SuccOrder β] → [WellFoundedLT β] → β → CategoryTheory.ObjectProperty C

Given P : ObjectProperty C, a family of categories J a, this is the transfinite iteration of Q ↦ Q.strictLimitsClosureStep J.

Defined in

Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryLinearOrderSuccOrderWellFoundedLT