{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} → [SizeOf C] → A.Hom B → ℕ