アーベル圏の埋め込み定理は圏論を
述語論理上に定式化した公理系から導かれる定理と言う訳じゃないでしょ

群論のCayleyの表現定理とかとほとんど事情は変わらんよ
難易度が違うだけで

>>509は見かけ上の高級さに騙されてるだけ