Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already familiar with either type theory or category theory.
Something I looked for on this very intriguing site was a reconciliation in my mind between dependent types and higher kinded types. This has been a nagging question since the announcement of Scala moving to the DOT calculus[1].<p>While this page[2] helped a bit, doing more research unveiled an example put out by Runar here[3].<p>Has anyone else considered a reasonable method for addressing what higher-kinded types provide currently in a DOT calculus, especially as it pertains to "matching" the type parameters in a higher-kinded type?<p>1 - <a href="http://lampwww.epfl.ch/~amin/dot/fool.pdf" rel="nofollow">http://lampwww.epfl.ch/~amin/dot/fool.pdf</a><p>2 - <a href="http://ncatlab.org/nlab/show/dependent+type+theory" rel="nofollow">http://ncatlab.org/nlab/show/dependent+type+theory</a><p>3 - <a href="https://gist.github.com/runarorama/33986541f0f1ddf4a3c7" rel="nofollow">https://gist.github.com/runarorama/33986541f0f1ddf4a3c7</a>
Also, see some of Robert Harper's lectures on the same subject: <a href="https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN" rel="nofollow">https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_Ync...</a>
See also Bob Harper's blog for a more leisurely exposition:<p><a href="https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/" rel="nofollow">https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...</a>