Here is a lecture series on HoTT from CMU. The video recordings are abysmal, but I still find the lectures very interesting because of how the instructor motivates everything.<p><a href="https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z" rel="nofollow">https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQB...</a>
A consequence of HOT in relation to programs is that you can compare programs for equality without running them. I rediscovered this a few years ago. It means that e.g. certain physical simulations could be known to not complete without running them to assumed termination. Currently we are wasting millions of dollars running simulations that we could show will not produce valid results.<p>HOT is an interesting development. You can fit all existing mathematics within it, in addition to mathematics we have not explored, such as systems where you do not accept the axiom of choice or, more interestingly, disregard it entirely.<p>It is constructive. This is interesting because it means real numbers "do not exist" as you can not write them down. Specific transcendental constants <i>can</i> be written down because you hold them by their relationship to other numbers.<p>I had hoped to study it and its application to number theory and computation but it is nearly impossible to get back into school.
Here's the shortest intro I know of:<p><a href="https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf" rel="nofollow">https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf</a>
"the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible)"<p>I'm sure Mr Hilbert would approve.<p>"and the formalization of each of these in computer proof assistants."<p>Aah, loosely IT related (hence the post) and surely Lean and co can't be far away from the discussion.<p>"As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux."<p>The WP article is quite dense for a civilian to get through so I hope something cool is on the horizon.<p>Is a result on the way or has Lean blue screened?