>**Implement a Categorical Theorem Prover.** Modern theorem provers for first-order logic are not particularly well-suited for reasoning about categories, which requires purely equational reasoning, empty sorts, ground completeness, and other niche features. The goal of this project is to implement a theorem prover specifically tailored to categorical needs.
I don't think such a feat is possible. I get the feeling, that since **Cat** is Cartesian Closed with Delta morphisms that general Categorical theorem proving might actually be undecidable.
The proof is would be simular to the ones given in, [
A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points](https://arxiv.org/pdf/math/0305282.pdf).