-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v, u₁} C} {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 :
    autoParam (∀ (i j : J) (h : i ≠ j), CategoryTheory.Mono (f i j h)) CategoryTheory.GlueData'.f_mono._autoParam}
  {f_hasPullback :
    autoParam (∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k), CategoryTheory.Limits.HasPullback (f i j hij) (f i k hik))
      CategoryTheory.GlueData'.f_hasPullback._autoParam}
  {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))}
  {J_1 : Type v} {U_1 : J_1 → C} {V_1 : (i j : J_1) → i ≠ j → C} {f_1 : (i j : J_1) → (h : i ≠ j) → V_1 i j h ⟶ U_1 i}
  {f_mono_1 :
    autoParam (∀ (i j : J_1) (h : i ≠ j), CategoryTheory.Mono (f_1 i j h)) CategoryTheory.GlueData'.f_mono._autoParam}
  {f_hasPullback_1 :
    autoParam
      (∀ (i j k : J_1) (hij : i ≠ j) (hik : i ≠ k), CategoryTheory.Limits.HasPullback (f_1 i j hij) (f_1 i k hik))
      CategoryTheory.GlueData'.f_hasPullback._autoParam}
  {t_1 : (i j : J_1) → (h : i ≠ j) → V_1 i j h ⟶ V_1 j i ⋯}
  {t'_1 :
    (i j k : J_1) →
      (hij : i ≠ j) →
        (hik : i ≠ k) →
          (hjk : j ≠ k) →
            CategoryTheory.Limits.pullback (f_1 i j hij) (f_1 i k hik) ⟶
              CategoryTheory.Limits.pullback (f_1 j k hjk) (f_1 j i ⋯)}
  {t_fac_1 :
    ∀ (i j k : J_1) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
      CategoryTheory.CategoryStruct.comp (t'_1 i j k hij hik hjk)
          (CategoryTheory.Limits.pullback.snd (f_1 j k hjk) (f_1 j i ⋯)) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f_1 i j hij) (f_1 i k hik))
          (t_1 i j hij)}
  {t_inv_1 :
    ∀ (i j : J_1) (hij : i ≠ j),
      CategoryTheory.CategoryStruct.comp (t_1 i j hij) (t_1 j i ⋯) = CategoryTheory.CategoryStruct.id (V_1 i j hij)}
  {cocycle_1 :
    ∀ (i j k : J_1) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
      CategoryTheory.CategoryStruct.comp (t'_1 i j k hij hik hjk)
          (CategoryTheory.CategoryStruct.comp (t'_1 j k i hjk ⋯ ⋯) (t'_1 k i j ⋯ ⋯ hij)) =
        CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f_1 i j hij) (f_1 i k hik))},
  { 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 } =
      { J := J_1, U := U_1, V := V_1, f := f_1, f_mono := f_mono_1, f_hasPullback := f_hasPullback_1, t := t_1,
        t' := t'_1, t_fac := t_fac_1, t_inv := t_inv_1, cocycle := cocycle_1 } →
    J = J_1 ∧ U ≍ U_1 ∧ V ≍ V_1 ∧ f ≍ f_1 ∧ t ≍ t_1 ∧ t' ≍ t'_1