Michael Makkai is the inventor of anafunctors and FOLDS, which are both ways of doing category theory and higher category theory without saying anything evil or requiring the axiom of choice. Makkai is also important in the category-theoretic approach to logic (which is mostly the approach that you see here on the -Lab).