While category theory is widely accepted for semantic analyses of programming languages, the use of formalised category theory is not widespread in computer science. Formalisations do exist in systems such as Mizar, Isabelle/HOL and NuPRL, but our focus is on the interactive programming and theorem-proving environment Coq, where formalisations by Saïbi/Huet and Simpson exist but are still not used for applications in computer science. An effort will be made to understand why this is so and to point to possible solutions. The mathematical problem is that of size and the additional computer-science problem that of equality of morphisms.