{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} →
          (val : A.obj ⟶ B.obj) →
            autoParam ((CategoryTheory.ConcreteCategory.hom (F.map val)) A.pt = B.pt)
                CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp._autoParam →
              A.Hom B