Category theory is an abstract branch of mathematics used to model mathematical "objects", and mappings between them.
In order to define a category you define the mathematical objects involved (such as "Sets" for instance), and the mappings (such as "Functions" for instance). So there is a category of mathematical sets and their functions.
Now the categories themselves could also be considered mathematical objects, and we could look at mappings between categories as well, which would also be a category.
In more detail a Category consists of:
Mappings (called morphisms) between those objects.
A binary composition operator, which can combine those mappings such that a mapping from object A to object B, and a mapping from object B to object C can be combined into a single mapping from object A to object C.
There should be a mapping that acts as an identity under composition, such that composing that mapping with another mapping M, gives you back the mapping M.
Composition should be associative.
Anything that can be represented by the above list can be analyzed as a category, that is why it is considered so abstract.
The Curry Howard isomorphism. The idea that logic and programming are just two sides of the same coin: types are propositions and programs are proofs.
Category Theory in Coq - Encodes category theory in Coq, with the primary aim being to allow representation and manipulation of categorical terms, as well realization of those terms in various target categories.