Right, ZFC. Almost all mathematicians accept the axiom of choice. The rest are minor nuances that most students won't even encounter and are only ever investigated by logicians. And even the difference between ZF with or without C only manifests with uncountable sets. This is not the case with type theory. AFAIK, the theories can differ on such questions like whether all subsets of a finite set are finite.

When mathematicians, not logicians, learn logic, it should be made to combine with what they actually do. Type theory is not quite there yet, and is still rather inaccessible and arcane, although that may change.

Turing was interested in making type theory approachable to mathematician, and came up with a gradual path to adoption in his 1944 unpublished manuscript The Reform of Mathematical Notation and Phraseology. He writes:

> It has long been recognised that mathematics and logic are virtually the same and that they may be expected to merge imperceptibly into one another. Actually this merging process has not gone at all far, and mathematics has profited very little from researches in symbolic logic. The chief reasons for this seem to be a lack of liaison between the logician and the mathematician-in-the-street. Symbolic logic is a very alarming mouthful for most mathematicians, and the logicians are not very much interested in making it more palatable. It seems however that symbolic logic has a number of small lessons for the mathematician which may be taught without it being necessary for him to learn very much of symbolic logic.

> In particular it seems that symbolic logic will help the mathematicians to improve their notation and phraseology, which are at present exceedingly unsystematic, and constitute a definite handicap both to the would-be-learner and to the writer who is unable to express ideas because the necessary notation for expressing them is not widely known.

> ... It would not be advisable to let the reform take the form of a cast-iron logical system into which all the mathematics of the future are to be expressed. No democratic mathematical community would stand for such an idea, nor would it be desirable. Instead one must put forward a number of definite small suggestions for improvement, each backed up by good argument and examples. It should be possible for each suggestion to be adopted singly. Under these circumstances one may hope that some of the suggestions will be adopted in one quarter or another, and that the use of all will spread.

In the preface to the manuscript, published in Collected Works of A.M. Turing, Volume 4: Mathematical Logic, 2001, Robin Gandy writes:

> Perhaps the most striking thing about this paper is its modesty. Turing was first and foremost a mathematician. He believed that the chief purpose of mathematical logic and the study of the foundations of mathematics was to help mathematicians to understand what they were doing, and could do. In pursuit of this goal, mathematical logicians must perforce construct and manipulate complex formal systems. But they have a duty to explain to mathematicians, in as non-technical way as possible, what they have accomplished. ... Turing disliked those high priests of logic who sought... to blind the mathematician-in-the-street with arcane formalisms.

It is my impression (and I'm not even a mathematician-in-the-street but a programmer-in-the-street) that type theory hasn't yet emerged out of the "high priest" stage.