Category theory
Note
Category theory can be written down in predicate logic (see below) or formulated within type theory. More or less well, it can also be modeled within set theory (see Category . set theory).
Direct axiomatization in logic
The nLab gives some formal definitions for categories as theory of concatenation in first order logic.
As opposed to the definition further below, this one has only one sort, namely what amounts to the $\mathrm{Arrow}$ types (see the types section below). The signature of the theory comes with two unary function symbols $s$ and $t$ as well as a ternary predicate $c$.
Read $s$ as source (or domain) and $t$ as target (or codomain). The intended interpretation of $c(f,g,h)$ is that $g$ concatenated with $f$ results in $h$. In the language below, that's $f\circ g = h$.
- Objects are eliminated by becoming the special arrows (identities), which are characterized as follows:
| rule | ${\large\frac{}{ ss(f) \, = \, s(f) \, = \, ts(f)\,\land\,tt(f) \, = \, t(f) \, = \, st(f)}}$ |
|---|
Conventionally, $s(f)$ and $t(f)$ would be of type $\mathrm{Obj}$, but one can simplify the axiomatization of category theory by noticing that objects $A$ are in a bijection with the identity morphisms $\mathrm{id}_A$. In more familar language, if $f$ is an arrow from an object $A$ to an object $B$, in the first-order axiomatization we have $s(f)=\mathrm{id}_A$. Thus $s(\mathrm{id}_A)=\mathrm{id}_A$.
- The operation $\circ$ only works on suitable arrows and what it does is concatenation:
| rule | ${\large\frac{ c(f,g,h) }{ s(f)\,=\,t(g)\,\land\,t(f)\,=\,t(h)\,\land\,s(g) \, = \, s(h) }}$ |
|---|---|
| rule | ${\large\frac{ s(f)\, =\, t(g) }{ \exists! h.\, c(f,g,h) }}$ |
- Axioms of identity and associativity for $\circ$:
| rule | ${\large\frac{}{ c(f,s(f),f) \land c(t(f),f,f)}}$ |
|---|---|
| rule | ${\large\frac{ c(f,g,j)\, \land\, c(g,h,k) }{ c(j,h,m)\ \leftrightarrow\ c(f,k,m) }}$ |
To clarify the last rule in terms of $\circ$, consider $(f\circ g) \circ h = f\circ (g \circ h)=m$ with $j:=f\circ g$ and $k:=g\circ h$.
To do some more complicated math (e.g. Cartesian products), one wants to add existence axioms of terminal objects and pullbacks. To speak of some set-like math one wants to add existence of a power object and “is element of” morphisms. One obtains the strength of a foundational system by adding initial objects and a law for detecting equality of morphisms, the computational feature of zero, successor, a notion of recursion and finally a variant of the axioms of choice.
Discussion
We now discuss variants of the definition using types.
A Definition using types
| rule | ${\large\frac{ }{ \mathrm{Category}\ :\ \mathrm{Type}}}$ |
| rule | ${\large\frac{ {\bf C}\ :\ \mathrm{Category} }{ \mathrm{Ob}_{\bf C}\ :\ \mathrm{Type}}}$ |
| rule | ${\large\frac{ A,\,B\ :\ \mathrm{Ob}_{\bf C} }{ {\bf C}[A,B]\ :\ \mathrm{Type} }}$ |
| rule | ${\large\frac{ A\ :\ \mathrm{Ob}_{\bf C} }{ 1_A\ :\ {\bf C}[A,A] }}$ |
| definiendum | $\circ:{\large\prod}_{\left({\bf C}\ :\ \mathrm{Category}\right)}{\large\prod}_{\left(A,\,B,\,C\ :\ \mathrm{Ob}_{\bf C}\right)}{\bf C}[A,B]\to{\bf C}[B,C]\to{\bf C}[A,C]$ |
| postulate | $1_B\circ f=f$ |
| postulate | $f\circ 1_A=f$ |
| postulate | $(f\circ g)\circ h=f\circ(g\circ h)$ |
We will use
| predicate | ${\bf C}$ … category $\equiv {\bf C}:\mathrm{Category}$ |
| predicate | $A\in{\bf C} \equiv {\bf C}:\mathrm{Ob}_{\bf C}$ |
The objects of a category will not necessarily be sets and so $A\in{\bf C}$ clearly is an overloading of the symbol '$\in$' with the set theoretic “is element of” predicate. As far as formalities go that's not very nice, but writing out $\mathrm{Ob}_{\bf C}$ every time isn't either.
Notation
The notation ${\bf C}[A,B]$ is pleasantly concise. On occasion, people write $\mathrm{Arrow}_{\bf C}(A,B)$ or $\mathrm{Mor}_{\bf C}(A,B)$. Arrows $A\to_{\bf C} B$ could also be used, but we'll stick to using them for type theoretical function types only. As a general comment, terms of ${\bf C}[A,B]$ are not necessarily functions and in even fewer cases are theory homomorphisms in the sense of algebra.
We write $[A,B]$ for internal homs, if they exist (then $A,B$ and $[A,B]$ all live in the same category).
Often, people write $\mathrm{Hom}_{\bf C}(A,B)$ for the Hom-sets, but we'll reserve that for Hom-functors. We will use $\mathrm{hom}_{\bf C}$ only for internal hom-functors.
Alternative definitions
Homs
Above we have dependent type ${\bf C}[A,B]:\mathrm{Type}$, where $A,B:\mathrm{Ob}_{\bf C}$. One could also set this up as a function
${\bf C}[-,-]:\mathrm{Ob}_{\bf C}\to \mathrm{Ob}_{\bf C}\to\mathrm{Type}$
or its uncurried version. This is essentially how the Hom-functors work anyway.
Technical comment on the underlying logic
Clearly, I didn't (but maybe should) work around strict categories, i.e. in this wiki I freely use '=' on object and arrows.
Either way, type theory underlying the definition of a cateogry is arguably already better than the classical first-order logic approach, because is makes concatenation a function and not a rule which relies on matching an arrow-codomain with another arrow-domain. In the latter case, we have to compare two objects of a category, which runs against the spirit to only consider things up to isomorphism.
Identity types
As discussed in Type theoretic definition of category, in type theory with identity types, we could state the three postulates as rules, witnessed by terms $\mathrm{rightUnit}$, $\mathrm{leftUnit}$ and $\mathrm{assoc}$.
Concatenation
Instead of setting up $\circ$ as a function, which could just take the existence of a term as a rule
${\large\frac{ f\ :\ {\bf C}[A,B]\ \ \ \ g\ :\ {\bf C}[B,C] }{ g\circ f\ :\ {\bf C}[A,C] }}$
The type of the concatenation function
As far as formal axiomatizations go, some require you to each time fix a cateogry ${\bf C}$ and a triple of its objects $A,B,C$ in the meta language, and then provide you with
$\circ^{\bf C}_{A,B,C}:{\bf C}[A,B]\to{\bf C}[B,C]\to{\bf C}[A,C]$.
Other axiomatizations require you to just fix a category ${\bf C}$ and make concatenation polymorphic over objects
$\circ^{\bf C}:\forall\left(A,B,C:\mathrm{Ob}_{\bf C}\right).\,{\bf C}[A,B]\to{\bf C}[B,C]\to{\bf C}[A,C]$.
Our axiomatization above defines $\circ$ for all categories at once. This then requires it to be polymorphic over two levels and so it must be dependently typed. (In intuitionistic type theory, the dependent product type $\Pi_{x:A}$ corresponds to universal quantization over $x$'s in the domain $A$.) We still use the indexed $\circ$ to denote for which category or object the operation has been instantiated, e.g. in opposite category.
Extended defintion
There is an alternative definition of categories which, instead of ${\bf C}[A,B]$, defines the type $\mathrm{Mor}_{\bf C}$ of all arrows of a category and fixes source and target via two functions $\mathrm{dom},\mathrm{codom}:\mathrm{Mor}_{\bf C}\to\mathrm{Ob}_{\bf C}$. This is convenient, for example, when we want to define a small category, in which both $\mathrm{Ob}_{\bf C}$ and $\mathrm{Mor}_{\bf C}$ are required to be proper sets. For this reason, we now add those notions to our theory by a sub-typing ${\bf C}[A,B] <: \mathrm{Mor}_{\bf C}$.
| rule | ${\large\frac{ {\bf C}\ :\ \mathrm{Category} }{ \mathrm{Mor}_{\bf C}\ :\ \mathrm{Type}}}$ |
| rule | ${\large\frac{ A,\,B\ :\ \mathrm{Ob}_{\bf C} }{ {\bf C}[A,B]\ <:\ \mathrm{Mor}_{\bf C} }}$ |
| rule | ${\large\frac{ f\ :\ {\bf C}[A,B] }{ \mathrm{dom}(f)\,=\,A\hspace{.5cm}\mathrm{codom}(f)\,=\,B }}$ |
The last rule fixes the compatibility of the overlapping definitions.
Reference
Wikipedia: Category (mathematics), Category theory
nLab: Category, Type theoretic definition of category, strict categories, Trimble on ETCS I, and links therein.
Haskell.org: Category theory & functional programming lecture notes
Categories and Setiods in Type Theory: arXiv link
A type theory of categories webpage link