{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S : J.Cover X} →
          {I₁ I₂ : S.Arrow} →
            {motive : I₁.Relation I₂ → Sort u_1} →
              ((Z : C) →
                  (g₁ : Z ⟶ I₁.Y) →
                    (g₂ : Z ⟶ I₂.Y) →
                      (w : CategoryTheory.CategoryStruct.comp g₁ I₁.f = CategoryTheory.CategoryStruct.comp g₂ I₂.f) →
                        motive { Z := Z, g₁ := g₁, g₂ := g₂, w := w }) →
                (t : I₁.Relation I₂) → motive t