∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A}
  (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.val)) (i₀ : E.I₀),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c)
      (F.val.map (E.f i₀).op) =
    c.ι i₀