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 were 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 likened to machine code (or assembly language) together with the function calls of an operating system kernel.  Category theory is then like the C programming language and its compiler.