Will Homotopy Type Theory ever be as accessible as traditional Set Theory? At the moment, Homotopy Type Theory is barely accessible to undergraduates, and only the most advanced or most gifted could have a decent chance of grasping it at a workable level without mountains of hard work. Even just understanding enough to be able to build up from it to "normal" mathematics is pretty much beyond me and all those I know, at this point.
Learning ZFC to the level required to define most of mathematics is child's play by comparison - until one gets to the Axiom Schema of Replacement I'd say there's scarcely much of a challenge at all. 
Is this a problem with the theory itself? Is it irreducibly difficult by its very nature? Will those without knowledge of Model Categories (Or whatever it is that is required) be forever barred from understanding this foundation?
Or is there a chance in the future that, given enough time, we may have found a way to present Homotopy Type Theory that gives it a level of accessibility comparable to ZFC? 
If this is a possibility, then how long as a lower bound would it likely take for the theory to reach such a level? 
I honestly believe that this is one of the main obstacles in the way of the theory becoming widely adopted, and I would like to believe that there might eventually be resources for this subject that aren't as tremendously difficult as those available now, but I do not know enough to say for sure if this is possible. 
 A: With tongue partly in my cheek, one possible answer is that the reason ZFC is "child's play" while HoTT is "barely accessible" to undergraduates has more to do with the rest of a standard undergraduate (and pre-college) education nowadays than with ZFC and HoTT themselves.  If working mathematicians come to appreciate and use type theory more, then mathematics will be formulated more in that style, and if high-school students learn a modern programming language, they will be much better-prepared to understand type theory.
Another answer is that the difficult parts of HoTT, like complicated HITs and univalence, are analogous to the difficult parts of ZFC, like Replacement and so on.  The fragment of HoTT that suffices for "ordinary" mathematics, e.g. type theory together with function extensionality, propositional truncation, and quotient types, ought to be much easier to understand.  (Unfortunately, the first edition of the HoTT book doesn't separate out this fragment very clearly.)  I know of people who teach type theories in place of set theories to undergraduates in their "intro to proofs" classes.
