@ Keith - I don't think they are asking to make a universal categorical theorem proving *algorithm*. They want something like Coq but specially tailored to category theory. The underlying theory for Coq is undecidable too. This is why these proof assistants need a lot of human effort to get them to prove anything significant.

While it looks like they want to stay away from FOL, Saul Feferman famously tried to formulate category theory in FOL for nearly 50 years. He built on an alternate formulation of set theory due to Quine called [New Foundations](https://en.wikipedia.org/wiki/New_Foundations). His idea was to use Quine's formulation so he could always have hom-sets and not worry about big categories. Here is a [recent review paper](https://arxiv.org/pdf/1603.03272.pdf) of his effort from 2016.

If you wanted to take this approach, it might be something to implement in Isabelle like Paulson's [Isabelle/ZF](http://isabelle.in.tum.de/library/ZF/index.html).

But Coq looks good enough for the [Homotopy Type Theory](https://homotopytypetheory.org/book/) research program. I'm a little curious why others aren't satisfied.

While it looks like they want to stay away from FOL, Saul Feferman famously tried to formulate category theory in FOL for nearly 50 years. He built on an alternate formulation of set theory due to Quine called [New Foundations](https://en.wikipedia.org/wiki/New_Foundations). His idea was to use Quine's formulation so he could always have hom-sets and not worry about big categories. Here is a [recent review paper](https://arxiv.org/pdf/1603.03272.pdf) of his effort from 2016.

If you wanted to take this approach, it might be something to implement in Isabelle like Paulson's [Isabelle/ZF](http://isabelle.in.tum.de/library/ZF/index.html).

But Coq looks good enough for the [Homotopy Type Theory](https://homotopytypetheory.org/book/) research program. I'm a little curious why others aren't satisfied.