∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {X Y : F.CoGrothendieck}
  (base : X.base ⟶ Y.base) (fiber : X.fiber ⟶ (F.map base.op.toLoc).toFunctor.obj Y.fiber) (base_1 : X.base ⟶ Y.base)
  (fiber_1 : X.fiber ⟶ (F.map base_1.op.toLoc).toFunctor.obj Y.fiber),
  ({ base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 }) = (base = base_1 ∧ fiber ≍ fiber_1)