Cubical sets and cubical categories are widely used in
mathematics and computer science, from homotopy theory to homotopy
type theory, higher-dimensional automata and, last but not least,
higher-dimensional rewriting, where our own interest in these
structures lies. To formalise cubical categories with the Isabelle/HOL
proof assistant along the path of least resistance, we take a
single-set approach to categories, which leads to new axioms for
cubical categories. Taming the large number of initial candidate
axioms has relied essentially on Isabelle's proof automation. Yet we
justify their correctness relative to the standard axiomatisation by
Al Agl, Brown and Steiner via categorical equivalence proofs outside
of Isabelle. In combination, these results present a case study in
experimental mathematics with a proof assistant. In this talk I will
focus on the formalisation experience -- lights and shadows -- and
conclude with some general remarks about formalised mathematics. This
is joint work with Philippe Malbos and Tanguy Massacrier (Université
Claude Bernard Lyon 1).
