∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D)
  (I : S.shape.R), (S.index P).fst I = P.map I.r.g₁.op