In fact. if such a generalized Categorical theorem prover existed, then a generalized Set theorem prover would also exist: simply truncate the result!

No such prover can exist since it would contradict Godelâ€™s First Incompleteness Theorem.

No such prover can exist since it would contradict Godelâ€™s First Incompleteness Theorem.