Should Type Theory Replace Set Theory as the Foundation of Mathematics?

Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (HoTT), is a preferable and should be considered as an alternative (Thorsten Altenkirch).

https://www.researchgate.net publication/368474630_Should_Type_Theory_Replace_Set_Theory_as_the_Foundation_of_Mathematics 

We refer the reader also to Bealer's interesting critique of sets in his book Quality and Concept. Our own finitist and computationalist position concerning foundations, as we have discussed before, is very critical of ZFC and highly favors dependent type theory (but not necessarily homotopy type theory) but also attaches value to Girard's system F (or its extensions) and second-order logic (cf. Simpson's reverse mathematics project) and to systems such as $HA^\omega$ (Heyting Arithmetic in all finite types) built over Gödel's system T.  We consider the concept of list (finite sequence) to be more fundamental than that of finite set - this is reflected in combinatorics. It would also be interesting to investigate a 'dialogical' foundations of mathematics (inspired by linear logic and functional interpretations as well as automatic theorem provers) in which proofs are replaced by dialogues in the style of Plato's Meno.

Category theory is not a foundations of mathematics, but it is close. Some suitable extension of dependent type theory can serve as a good foundations which we can liken to machine code (or assembly language) together with the system calls of an operating system kernel.  Category theory is then like the C programming language and its compiler.  

It is interesting to note that it does not seem that second-order logic or even certain extensions of second-order logic are natural or suitable as a foundation for even basic areas of modern mathematics, even from a finitist (enumerable) perspective. Even if we consider only countable rings of cardinality $N$ - or consider elementary number theory - we are lead to quickly to the cardinality $PPN$ if we wish to consider something as simple as a quotient ring $R/ I$ which is a set of subsets of $R$. Also in modular arithmetic we are in fact dealing with relations between congruence classes, thus going beyond second-order logic. The same phenomenon is likely true for category theory, even if quotient constructions can be formalized without the leap into $PPN$.  It would be interesting to check if Euclid has natural third-order constructions. The lesson is that we should abandon extensionalism and use a functional interpretation of such higher-order constructions. This is what Coq and Agda do and we should investigate in detail anticipations of such an approach in ancient philosophy.