{C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    {motive : CategoryTheory.GlueData' C → Sort u} →
      ((J : Type v) →
          (U : J → C) →
            (V : (i j : J) → i ≠ j → C) →
              (f : (i j : J) → (h : i ≠ j) → V i j h ⟶ U i) →
                (f_mono : ∀ (i j : J) (h : i ≠ j), CategoryTheory.Mono (f i j h)) →
                  (f_hasPullback :
                      ∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k),
                        CategoryTheory.Limits.HasPullback (f i j hij) (f i k hik)) →
                    (t : (i j : J) → (h : i ≠ j) → V i j h ⟶ V j i ⋯) →
                      (t' :
                          (i j k : J) →
                            (hij : i ≠ j) →
                              (hik : i ≠ k) →
                                (hjk : j ≠ k) →
                                  CategoryTheory.Limits.pullback (f i j hij) (f i k hik) ⟶
                                    CategoryTheory.Limits.pullback (f j k hjk) (f j i ⋯)) →
                        (t_fac :
                            ∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
                              CategoryTheory.CategoryStruct.comp (t' i j k hij hik hjk)
                                  (CategoryTheory.Limits.pullback.snd (f j k hjk) (f j i ⋯)) =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Limits.pullback.fst (f i j hij) (f i k hik)) (t i j hij)) →
                          (t_inv :
                              ∀ (i j : J) (hij : i ≠ j),
                                CategoryTheory.CategoryStruct.comp (t i j hij) (t j i ⋯) =
                                  CategoryTheory.CategoryStruct.id (V i j hij)) →
                            (cocycle :
                                ∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
                                  CategoryTheory.CategoryStruct.comp (t' i j k hij hik hjk)
                                      (CategoryTheory.CategoryStruct.comp (t' j k i hjk ⋯ ⋯) (t' k i j ⋯ ⋯ hij)) =
                                    CategoryTheory.CategoryStruct.id
                                      (CategoryTheory.Limits.pullback (f i j hij) (f i k hik))) →
                              motive
                                { J := J, U := U, V := V, f := f, f_mono := f_mono, f_hasPullback := f_hasPullback,
                                  t := t, t' := t', t_fac := t_fac, t_inv := t_inv, cocycle := cocycle }) →
        (t : CategoryTheory.GlueData' C) → motive t