{S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        {motive : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰 → Sort u_3} →
          ((functor : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme) →
              (natTrans : functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰) →
                (equifibered : CategoryTheory.NatTrans.Equifibered natTrans) →
                  motive { functor := functor, natTrans := natTrans, equifibered := equifibered }) →
            (t : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰) → motive t