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. |