∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X)
  {X_1 Y : CategoryTheory.Over f} (κ : X_1 ⟶ Y), f.iteratedSliceForward.map κ = CategoryTheory.Over.homMk κ.left.left ⋯