-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.mk.injEq : ∀ {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)