Sure, but is discarding Type Theory and Category Theory really fair with a phrase like "All of modern mathematics"? Especially in terms of a connection with computer science.