Started a coq module for category theory.