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