-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }))
  (hom :
    ⦃Y : C⦄ →
      (q : Y ⟶ S) →
        ⦃i₁ i₂ : ι⦄ →
          (f₁ : Y ⟶ X i₁) →
            (f₂ : Y ⟶ X i₂) →
              autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                  CategoryTheory.Pseudofunctor.DescentData._auto_1 →
                autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                    CategoryTheory.Pseudofunctor.DescentData._auto_3 →
                  ((F.map f₁.op.toLoc).toFunctor.obj (obj i₁) ⟶ (F.map f₂.op.toLoc).toFunctor.obj (obj i₂)))
  (pullHom_hom :
    autoParam
      (∀ ⦃Y' Y : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) (hq : CategoryTheory.CategoryStruct.comp g q = q')
        ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂)
        (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁) (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
        CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom q f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ =
          hom q' gf₁ gf₂ ⋯ ⋯)
      CategoryTheory.Pseudofunctor.DescentData.pullHom_hom._autoParam)
  (hom_self :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (x : CategoryTheory.CategoryStruct.comp g (f i) = q),
        hom q g g ⋯ ⋯ = CategoryTheory.CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (obj i)))
      CategoryTheory.Pseudofunctor.DescentData.hom_self._autoParam)
  (hom_comp :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
        (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q),
        CategoryTheory.CategoryStruct.comp (hom q f₁ f₂ hf₁ hf₂) (hom q f₂ f₃ hf₂ hf₃) = hom q f₁ f₃ hf₁ hf₃)
      CategoryTheory.Pseudofunctor.DescentData.hom_comp._autoParam)
  (obj_1 : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }))
  (hom_1 :
    ⦃Y : C⦄ →
      (q : Y ⟶ S) →
        ⦃i₁ i₂ : ι⦄ →
          (f₁ : Y ⟶ X i₁) →
            (f₂ : Y ⟶ X i₂) →
              autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                  CategoryTheory.Pseudofunctor.DescentData._auto_1 →
                autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                    CategoryTheory.Pseudofunctor.DescentData._auto_3 →
                  ((F.map f₁.op.toLoc).toFunctor.obj (obj_1 i₁) ⟶ (F.map f₂.op.toLoc).toFunctor.obj (obj_1 i₂)))
  (pullHom_hom_1 :
    autoParam
      (∀ ⦃Y' Y : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) (hq : CategoryTheory.CategoryStruct.comp g q = q')
        ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂)
        (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁) (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
        CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom_1 q f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ =
          hom_1 q' gf₁ gf₂ ⋯ ⋯)
      CategoryTheory.Pseudofunctor.DescentData.pullHom_hom._autoParam)
  (hom_self_1 :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (x : CategoryTheory.CategoryStruct.comp g (f i) = q),
        hom_1 q g g ⋯ ⋯ = CategoryTheory.CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (obj_1 i)))
      CategoryTheory.Pseudofunctor.DescentData.hom_self._autoParam)
  (hom_comp_1 :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
        (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q),
        CategoryTheory.CategoryStruct.comp (hom_1 q f₁ f₂ hf₁ hf₂) (hom_1 q f₂ f₃ hf₂ hf₃) = hom_1 q f₁ f₃ hf₁ hf₃)
      CategoryTheory.Pseudofunctor.DescentData.hom_comp._autoParam),
  ({ obj := obj, hom := hom, pullHom_hom := pullHom_hom, hom_self := hom_self, hom_comp := hom_comp } =
      { obj := obj_1, hom := hom_1, pullHom_hom := pullHom_hom_1, hom_self := hom_self_1, hom_comp := hom_comp_1 }) =
    (obj = obj_1 ∧ hom ≍ hom_1)