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

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-possible-to-formulate-category-theory-without-set-theory https://math.stackexchange.com/questions/1519330/is-it-possi... [2] https://medium.com/@calhoun137/a-programmers-way-of-thinking-about-sets-and-categories-3f10ef2fa72c https://medium.com/@calhoun137/a-programmers-way-of-thinking...