{C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (J : Type v) →
      (U : J → C) →
        (V : J × J → C) →
          (f : (i j : J) → V (i, j) ⟶ U i) →
            autoParam (∀ (i j : J), CategoryTheory.Mono (f i j)) CategoryTheory.GlueData.f_mono._autoParam →
              (f_hasPullback :
                  autoParam (∀ (i j k : J), CategoryTheory.Limits.HasPullback (f i j) (f i k))
                    CategoryTheory.GlueData.f_hasPullback._autoParam) →
                autoParam (∀ (i : J), CategoryTheory.IsIso (f i i)) CategoryTheory.GlueData.f_id._autoParam →
                  (t : (i j : J) → V (i, j) ⟶ V (j, i)) →
                    (∀ (i : J), t i i = CategoryTheory.CategoryStruct.id (V (i, i))) →
                      (t' :
                          (i j k : J) →
                            CategoryTheory.Limits.pullback (f i j) (f i k) ⟶
                              CategoryTheory.Limits.pullback (f j k) (f j i)) →
                        (∀ (i j k : J),
                            CategoryTheory.CategoryStruct.comp (t' i j k)
                                (CategoryTheory.Limits.pullback.snd (f j k) (f j i)) =
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f i j) (f i k))
                                (t i j)) →
                          (∀ (i j k : J),
                              CategoryTheory.CategoryStruct.comp (t' i j k)
                                  (CategoryTheory.CategoryStruct.comp (t' j k i) (t' k i j)) =
                                CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f i j) (f i k))) →
                            CategoryTheory.GlueData C