In this article, we show how one can formalise in type theory mathematical objects, for which dependent types are usually deemed unavoidable, using only simple types. We outline a method to encode most of the terms of Lean’s dependent type theory into the simple type theory of Isabelle/HOL. Taking advantage of Isabelle’s automation, we illustrate our method with the formalisation in Isabelle/HOL of a mathematical notion developed in the 1980s: strict omega-categories. Strict omega-categories are generalisations of strict $n$-categories. According to Ross Street, $n$-categories were first introduced by John Roberts as coefficient structures to define non-abelian cohomology in the context of algebraic quantum field theory.