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.