圏論の定式化が、ZFC で十分という話を聞いたことがあります。
僕の経験からすると、その通りです。
ただ、圏論の定式化は、BGC、もしくは BGE の方がやりやすいです。
もちろん、BGE は ZFC の保存拡大ですから、
最終的には ZFC の言葉で記述できます。
（ ZFC に、= と ∈ 以外の述語記号や、そのほかの関数記号を導入しても、
BGE の方にはそれに対応して、class constant を導入すればいいですから、
この場合でも、BGE が ZFC の保存拡大であることが、ルーチンに証明できます。）
というよりも、ZFC には収まりきらない圏論の定式化というものがあるとしたら、
それは、どれだけ強力な公理を設定しているのかと、かえって疑問に思えます。
