∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J],
  AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F =
    { J := Shrink.{u, w} J, U := fun j => F.obj ((equivShrink J).symm j),
      V := fun ij =>
        ↑(AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm ij.1) ((equivShrink J).symm ij.2)),
      f := fun i j =>
        (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, j).1)
            ((equivShrink J).symm (i, j).2)).ι,
      f_mono := ⋯, f_hasPullback := ⋯, f_id := ⋯,
      t := fun i j => AlgebraicGeometry.Scheme.IsLocallyDirected.t F ((equivShrink J).symm i) ((equivShrink J).symm j),
      t_id := ⋯,
      t' := fun i j k =>
        CategoryTheory.Limits.pullback.lift
          (AlgebraicGeometry.IsOpenImmersion.lift
            (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm j) ((equivShrink J).symm k)).ι
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst
                (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, j).1)
                    ((equivShrink J).symm (i, j).2)).ι
                (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, k).1)
                    ((equivShrink J).symm (i, k).2)).ι)
              (AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F ((equivShrink J).symm i) ((equivShrink J).symm j)))
            ⋯)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst
              (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, j).1)
                  ((equivShrink J).symm (i, j).2)).ι
              (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, k).1)
                  ((equivShrink J).symm (i, k).2)).ι)
            (AlgebraicGeometry.Scheme.IsLocallyDirected.t F ((equivShrink J).symm (i, j).1)
              ((equivShrink J).symm (i, j).2)))
          ⋯,
      t_fac := ⋯, cocycle := ⋯, f_open := ⋯ }