a fantastic simplification of our subject

I can't make Mike's proof type-check, so let me try the following: For any set-valued functor, T, from any category, let a:O -> T be the unique transformation from the empty functor. Isn't it obviously cartesian? Has Mike shown all set-valued functors are empty? Good heavens.