The Stack Exchange bot reminded me that I had committed myself to asking some questions, but please allow a possibly naive question, possibly of a philosophical nature rather than mathematical/computer-theoretical.
So, is it conceivable that the development of proof assistants make mainstream mathematicians switch their framework, from a set theoretical one, to a type theoretical one.
It is not that mathematicians all know about the axioms of ZFC, I'm certain most don't and most don't care, but mathematics are full of idiosyncratic set-theoretical gimmicks such as saying that a group is a 3-tuple consisting of a set, a law, a neutral element, and some people (most students) pay attention to the fact that it is a 3-tuple and not something else. (I have been asked which component of a similar 5-tuple a submodule should be…)
Type theory (especially how it is implemented) simultaneously departs from such constructions, and insists on the list of objects/axioms (so that the computer-definition of a group also contains a proof of associativity, etc.).
On the other hand, the concept of a set is clearly an important one.
Similarly, some constructions are built on sets in a way which might look unnatural — say defining the quotient set as a set of equivalence classes — but are now well understood, and can be avoided by a more categorical point of view.
I also have in mind more advanced notions of algebra/number theory where set theoretical notions look less avoidable, such as the definition of an ideal. (One could try to replace them by the epimorphism to the quotient ring, but that does not look very easy to handle.)