∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
  {fiber : CategoryTheory.Functor C (Type w)}
  {isCofiltered :
    autoParam (CategoryTheory.IsCofiltered fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam}
  {initiallySmall :
    autoParam (CategoryTheory.InitiallySmall fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam}
  {jointly_surjective : ∀ {X : C}, ∀ R ∈ J X, ∀ (x : fiber.obj X), ∃ Y f, ∃ (_ : R.arrows f), ∃ y, fiber.map f y = x}
  {fiber_1 : CategoryTheory.Functor C (Type w)}
  {isCofiltered_1 :
    autoParam (CategoryTheory.IsCofiltered fiber_1.Elements)
      CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam}
  {initiallySmall_1 :
    autoParam (CategoryTheory.InitiallySmall fiber_1.Elements)
      CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam}
  {jointly_surjective_1 :
    ∀ {X : C}, ∀ R ∈ J X, ∀ (x : fiber_1.obj X), ∃ Y f, ∃ (_ : R.arrows f), ∃ y, fiber_1.map f y = x},
  { fiber := fiber, isCofiltered := isCofiltered, initiallySmall := initiallySmall,
        jointly_surjective := jointly_surjective } =
      { fiber := fiber_1, isCofiltered := isCofiltered_1, initiallySmall := initiallySmall_1,
        jointly_surjective := jointly_surjective_1 } →
    fiber = fiber_1