∀ {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) (j : κ.ord.ToType),
  CategoryTheory.SmallObject.ιFunctorObj I.homFamily
      (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj (CategoryTheory.Arrow.mk f)).hom =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.relativeCellComplexιObj I κ f).F.map (CategoryTheory.homOfLE ⋯))
      (CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso I κ f j).hom