Category theory using 2-sorted logic

76 Views Asked by At

Can anyone give some reference text that axiomatizes category theory using first order logic using 2 sorts (if that makes sense)? I have found reference about 1 sorted axiomatization but I also found that 1 sorted and 2 sorted axiomatizations are not exactly the same. I am studying set theory built from category theory (ETCS) so I would like axiomatizations be built not in ZFC metatheory, but in some weak theory like PRA.

I would also appreciate any comments about it, for example, how perspective and useful set theory built from category theory is.