∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f)
      ((CategoryTheory.SmallObject.ιIteration I κ).app (CategoryTheory.Arrow.mk f)).right =
    ((CategoryTheory.SmallObject.iteration I κ).obj (CategoryTheory.Arrow.mk f)).hom