3 ms·

I'm not sure what you are basing this on. How can you judge that if you do not understand the theory or the motivation behind it? Because chapter 2 seemed like

• auggierose 13y ago
  I know that we are already very well capable of doing succinct proofs in interactive theorem proving systems like Isabelle that have a strong resemblance to "human" proofs. None of the proofs displayed in HoTT or the accompanying sources look shorter or more succinct than stuff I could do without HoTT. So HoTT might solve a problem for constructivists working with Coq. Problems you can entirely avoid by not working constructively (or with Coq, for that matter). Therefore, at this point, there is no evidence at all that HoTT might improve the state of the art in interactive theorem proving. That does not mean that this evidence might not come up at some point. How can I be sure in my judgement? Well, I don't have to understand string theory to be sure at this point that it is not relevant to interactive theorem proving. I would change my mind if somebody points out evidence that string theory is actually of major relevance to interactive theorem proving. Edit: I would even start learning string theory then.