∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} {E F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A)
  {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c)
  (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) {Z : A}
  (h : (E.multicospanIndex P).left a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (CategoryTheory.CategoryStruct.comp (c.ι a) h) =
    CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (CategoryTheory.CategoryStruct.comp (P.map (f.h₀ a).op) h)