{C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    {motive : CategoryTheory.GlueData C → Sort u} →
      ((J : Type v) →
          (U : J → C) →
            (V : J × J → C) →
              (f : (i j : J) → V (i, j) ⟶ U i) →
                (f_mono : ∀ (i j : J), CategoryTheory.Mono (f i j)) →
                  (f_hasPullback : ∀ (i j k : J), CategoryTheory.Limits.HasPullback (f i j) (f i k)) →
                    (f_id : ∀ (i : J), CategoryTheory.IsIso (f i i)) →
                      (t : (i j : J) → V (i, j) ⟶ V (j, i)) →
                        (t_id : ∀ (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)) →
                            (t_fac :
                                ∀ (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)) →
                              (cocycle :
                                  ∀ (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))) →
                                motive
                                  { J := J, U := U, V := V, f := f, f_mono := f_mono, f_hasPullback := f_hasPullback,
                                    f_id := f_id, t := t, t_id := t_id, t' := t', t_fac := t_fac,
                                    cocycle := cocycle }) →
        (t : CategoryTheory.GlueData C) → motive t