initial checkin of coq-categories library