FOLDS (first-order logic with dependent sorts) is a form of (intuitionistic or classical) predicate logic with a weak form of equality in which category theory (and even higher category theory) can be formulated but it is impossible to say anything evil. It was developed by Michael Makkai.