Theorems · Definition · category theory

CategoryTheory.SmallObject.SuccStruct.arrowSucc

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [SuccOrder J] → {j : J} → CategoryTheory.Functor (↑(Set.Iic j)) C → (i : J) → i < j → CategoryTheory.Arrow C

Given a functor F : Set.Iic j ⥤ C and i : J such that i < j, this is the arrow F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩.

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Cited by

8 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

CategoryTheory.CategoryLinearOrderSuccOrder