I really like this idea! I first got into type theory as a result of an answer by Carl Mummert to a question I asked on Math StackExchange[1]. I even wrote a blog post about it a year later[2].

Ever since then, I have considered type theory to be my favorite version of the foundations of math. I have often played around in theoretical foundations theory to discover as many connections as possible between foundations of math and computer science. That being said, I think the perspectives offered by set theory and category theory are extremely valuable, and that these three approaches compliment each other, and sometimes one is better than another for a specific purpose.

This is the first time I had really seen the possibility to reformulate computer science to bring it closer to mathematics. How exciting!

[1] https://math.stackexchange.com/questions/1519330/is-it-possi...

[2] https://medium.com/@calhoun137/a-programmers-way-of-thinking...