{𝒮 : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
    (𝒳 : CategoryTheory.BasedCategory 𝒮) →
      (𝒴 : CategoryTheory.BasedCategory 𝒮) → [SizeOf 𝒮] → SizeOf (CategoryTheory.BasedFunctor 𝒳 𝒴)