{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        {X A : C} → (A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X) → (F.obj X).carrier → (A ⟶ X)