As a non-mathematician, I'm confused how category theory relates back to formal systems. Is it its own formal system, or is it built on top of ZFC or type theory? If it's built on top of something else, what sort of algorithm would tell me whether the DAG that constitutes a proof from a set of axioms to a theorem involves category theory or not?