12
$\begingroup$

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.

$\endgroup$
7
  • 2
    $\begingroup$ Just a comment: I don't actually think that HoTT uses any algebraic topology. It uses, to my knowledge, the theory of model categories which are to homotopical algebra what abelian categories are to homological algebra. There's a chance @Qiaochu will know about this. $\endgroup$ Commented Feb 19, 2016 at 12:36
  • $\begingroup$ @AlexYoucis My mistake, I'll amend that $\endgroup$
    – Nethesis
    Commented Feb 19, 2016 at 12:37
  • 2
    $\begingroup$ Perhaps when scholars in HTT can explain what is that without needing lines and lines of very technical and specialized names, that will be understood perhaps only after reading several pages. It also seems to be a subject highly specialized of some kind of mathematical logic and, in particualr, of computer science. Until someone shows some very interesting result applied to more interesting or widely done mathemtatics, it will probably remain an obscure, unknown subject for very specialized specialists. This is my opinion. $\endgroup$
    – DonAntonio
    Commented Feb 19, 2016 at 12:37
  • 1
    $\begingroup$ @AlexYoucis Let's distinguish between the model theory of HoTT and HoTT itself. The former uses model categories, the latter does not. $\endgroup$
    – Zhen Lin
    Commented Feb 19, 2016 at 12:48
  • 1
    $\begingroup$ That's a bit more difficult. There is no single "homotopy type theory" at the moment. One reason is that we don't yet have a sufficiently general mathematical definition of higher inductive type – so instead of postulating that all higher inductive types exist (whatever that might mean), we are forced to postulate each one we want separately. Regardless, there is a basic/core system which you can find described in e.g. the appendix of the HoTT book. But please keep in mind that HoTT is not a first order theory or anything like that. $\endgroup$
    – Zhen Lin
    Commented Feb 19, 2016 at 12:57

1 Answer 1

14
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ I do feel that it would be helpful if that fragment were separated out, though I can think of reasons why in the HTT book it would not be. Do you know of any plans to make a more accessible book? I can understand the need to have one that does go into the attractions of HTT such as higher inductive types, but I do feel there is a need for one that simply aims to cover existing mathematics in a more type theoretic light. Among other things, it could work as a bit of a gateway to less familiar territory. $\endgroup$
    – Nethesis
    Commented Feb 19, 2016 at 19:42
  • $\begingroup$ Or do you feel the HTT book alone should be able to fulfil all needs? $\endgroup$
    – Nethesis
    Commented Feb 19, 2016 at 20:09
  • 4
    $\begingroup$ I personally hope that one day there will be a second edition of the HoTT Book which is a little better in this regard, but I know of no concrete plans for such a thing yet. I also do not know of any plans to write another book about HoTT. But there's certainly no reason to expect that a single book about HoTT should fulfill the needs of all readers, any more than it could for any other subject. $\endgroup$ Commented Feb 19, 2016 at 20:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .