$\DeclareMathOperator{\Id}{Id} \DeclareMathOperator{\Obj}{Obj} \DeclareMathOperator{\Arr}{Arr} \DeclareMathOperator{\Dom}{Dom} \DeclareMathOperator{\Cod}{Cod}$
MacLane defines "metacategories" purely axiomaticaly. When we look at it from perspective of first order logic we see that "metacategories" is a first order theory consisting following signature:
- two unary predicates $\Obj,\Arr$
- two unary functions $\Dom,\Cod$
- binary function $\circ$
- unary function $\Id$
and axioms for domain, codomain, composition unity. I wrote this axioms in the appendix.
Next, we can define a category as a model in this first order theory. Given two categories, we can also define a functor as a structure map.
Question. Is there some source which treats the whole category theory from this point of view?
For example I do not know how to define natural transformation in this language.
Appendix. Axioms for category theory :
- $(\forall f)(\Arr(f) \rightarrow (\Obj(\Dom(f)) \wedge \Obj((\Cod(f)))$
- $(\forall f,g)((\Arr(f)\wedge\Arr(g)\wedge\Cod(f)=\Dom(g))\rightarrow \Arr(g\circ f))$
- $(\forall a)(\Obj(a)\rightarrow((\Arr(\Id(a))\wedge \Dom(\Id(a))=a=\Cod(\Id(a))\wedge (\forall f)(\Arr(f)\rightarrow ((\Dom(f)=a\rightarrow f\circ\Id(a)=f)\wedge(\Cod(f)=a\rightarrow \Id(a)\circ f=f))))$
- $(\forall f,g,h)((\Arr(f)\wedge\Arr(g)\wedge\Arr(h)\wedge\Cod(f)=\Dom(g)\wedge \Cod(g)=\Dom(h))\rightarrow h\circ ((g\circ f) = (h\circ g)\circ f))$