∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (obj : Type u₂)
  (category : autoParam (CategoryTheory.Category.{v₂, u₂} obj) CategoryTheory.BasedCategory.category._autoParam)
  (p : CategoryTheory.Functor obj 𝒮) (obj_1 : Type u₂)
  (category_1 : autoParam (CategoryTheory.Category.{v₂, u₂} obj_1) CategoryTheory.BasedCategory.category._autoParam)
  (p_1 : CategoryTheory.Functor obj_1 𝒮),
  ({ obj := obj, category := category, p := p } = { obj := obj_1, category := category_1, p := p_1 }) =
    (obj = obj_1 ∧ category ≍ category_1 ∧ p ≍ p_1)