Homotopy Type Theory - unifying computation and mathematics at the base

[kram1032]

Type Theory has for a while had the potential to replace (Zermelo Fraenkel) set theory as a foundation for mathematics. It allows to manipulate proofs just like programs which makes Type Theory especially attractive for automated theorem checking or -proving and other such applications and it even potentially enables programmers to mathematically prove bug-freeness of at least certain classes of bugs: No thread-blocking-issues, no memory-leaks, no out-of-bound arrays... These things can become provable using Type Theory.

Fairly recently, the concept of Types has been associated with the concept of Homotopy which is a certain topological notion. Two geometric structures are homotopically equal, if there exists a continuous function that maps one object into the other. (There is the stronger notion of Isotopy which requires that such a transformation does not have any points of the geometric objects intersect with each other during the transformation, so for instance, the intervals [a,b] and [b,a] are not isotopic but they are homotopic by the continuous function in t: [a (1-t)+b t, b(1-t) + a t] - note that the end points swap places and so must, at some point, pass through each other. - Namely at t=1/2)

Through concepts from Homotopy, you gain several interesting things. Two of which are:
For one, you end up with a certain kind of equality which makes all isomorphic structures equal to each other (something that is highly wanted, since you don't typically care in which way, say, the integers are defined. As long as all definitions share certain properties, integers will still be integers. But if you don't have isomorphisms as equal, this will not be obvious.)
And for another you gain some notion of "higher dimensional types" which are notions that, as far as I understood it, would be almost impossible to emulate in set-theory.

A simple type "A" would be a "point"-like object. A type "A -> B" would be somewhat like a line. A type (A->B)->(C->D) would be equivalent to a plane. - at least to my current understanding. I'm pretty sure, I'm grossly oversimplifying here.

Anyway, last year was entirely dedicated to further the development of Homotopy Type Theory and amongst many fruitful papers for once, several of the people working in this field have teamed up to also release a fully freely available (online) book (you can also pay for a printed version if you so choose)
http://homotopytypetheory.org/book/

and a carnegie mellon lecture on the topic
http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%2207756bb0-b872-4a4a-95b1-b77ad206dab3%22

the styles of the book and the lecture differ quite a bit. The book starts directly with type theory and develops all else from there. The lecture starts with logic and highlighting the differences between "classical" logic and the kind of logic you get through this system.

[jehovajah]

Thans for the links Keam1032.

I do not know what to expect, but I do know Norman Wildberger has built his mathematical structure on types!

When I learned programming the meaning of type was quite clear : short, long double long etc. later when learning Quickbasic and c++ I found and loved the struct type and the pointer type( c++). I spent a good while implementing a pointer type in Quickbasic using the native perk and poke commands. I did not want to get into machine code etc..
Now I have lost contact with all the types out there, since memory is no longer a bottleneck!

I welcome this development because I feel mathematics is dying or dead! The mathematics I grew up with has stultified. The New Maths I was introduced to has also failed. I believe computational science is the natural subject for the former mathematical subject area.

Computational science, as in say Geolgebra, Mathematica etc actually balances out our understanding of what we do that we call athematical. Many terms like Homotopy sound new but they are McIntyre terms found in say Euclids Stoikeia or Apollonius Conics. It is this disconnect caused by arrogant use of Algebra that has cut away the natural connection between our senses and our manipulation in calculus of what we can sense!

When I programme, especially now, I use labels that mean something, so when I read the code I know what I was thinking! I know one cn comment but I prefer to see directly what I am calculating. Yea for unlimited data types!

[kram1032]

well, yeah, type theory isn't quite new. Nor is homotopy theory. Their combination, however, is. It's pretty much cutting edge maths.
Check out the lecture if you can sit through that. I think, he does a great job explaining what's different about it compared to the "usual", set-theoretic approach.
As said, he begins with logics, highlighting the differences between the classical logic which most know about, with the axioms of the law of the excluded middle (all propositions must be either true or false) or the double negation (what is not false must be true), and constructive logic which rejects the universal truths of those axioms.
(Notably, it doesn't at all reject their occasional existence. It just says that they are not always true.)

And starting from the notation used within classical logic, step by step, he introduces connections to either type-theory or homotopy theory and, in the process, replaces the notation of logic by the notation typically used in homotopy type theory.
I'm not very far into it yet (23 videos with ~75min each isn't easy to sit through) but it's already picking up.

He himself mentions that the book is great but he isn't convinced that it is easy enough to follow for newcommers. His course is only roughly based on the book.

[hobold]

This is very abstract stuff. But as one of my professors used to say: "abstraction empowers!"

I am only a handful of pages into the book, but it already seems to me these concepts could lead to a new generation of compilers, capable of more abstract and more powerful optimizations. This is a very interesting road to follow.

[kram1032]

If you watch the lectures, he repeatedly references "the five stages of constructive mathematics".
This isn't directly relevant to homotopy type theory, but since that is a constructive theory, you should probably also understand constructivity.
The talk he is refering to is this:
http://video.ias.edu/members/1213/0318-AndrejBauer

[kram1032]

The book itself continuously gets updated/corrected by the way. You can find the newest version here: https://github.com/HoTT

[kram1032]

Here's another video on the topic. This one tries to be a very short summary and to show the cutting edge research and current limitations of HoTT. It points out more clearly than other places I found so far what still is work in progress.

<a href="http://www.youtube.com/v/ziN2XcK5-PQ&rel=1&fs=1&hd=1" target="_blank">http://www.youtube.com/v/ziN2XcK5-PQ&rel=1&fs=1&hd=1</a>

[kram1032]

As said, Homotopy type theory combines the concepts of "Type", "homotopy" and "Category" into one thing. Of those three, I found that people think Categories are the hardest / the most confusing. Part of this combination means that all three subjects get a much clearer, more insightful description.

Here I found a video that talks about Category theory. It doesn't really explain how exactly they work, it's not an introduction to the minutest of details of the concept of categories.
What it is, is an appetizer of sorts. It broadly introduces what can be done with Categories and why they are interesting. - Applications reach from computational sciences over physics to modern biology.

<a href="http://www.youtube.com/v/p9VmyR-OMpM&rel=1&fs=1&hd=1" target="_blank">http://www.youtube.com/v/p9VmyR-OMpM&rel=1&fs=1&hd=1</a>

On a side note: youtube videos are apparently not recognized when you use https:// to link to them. And I wish this forum knew how to handle HTML5 players, for the sake of being future proof.

[kram1032]

Here is very early work on the subject - all in all, it's less than a decade years old!
This video shows well, what motivated the work on the subject; what it tries to solve.

<a href="http://www.youtube.com/v/kkKTW-Q0qkc&rel=1&fs=1&hd=1" target="_blank">http://www.youtube.com/v/kkKTW-Q0qkc&rel=1&fs=1&hd=1</a>

The quality is really low (240p) but fortunately the slides are written in such a huge font that you can still read it all. The first few minutes there are an introduction of the speaker and some technical difficulties. If you want to skip that, go to 5:59. The whole talk is designed for a non-mathematical audience. It practically doesn't use fancy notation beyond maybe a slide or two, and when it does, it's well explained what that notation is about.

[jehovajah]

Kram1032 asked me to add this video here.
 In the thread on the Vorrede to the Ausdehnungslehre 1844 it appears as a comment on my translation of a piece of that text.

http://www.fractalforums.com/complex-numbers/the-theory-of-stretchy-thingys/msg71668/#msg71668

[kram1032]

You didn't read the last post, did you? I already added it myself

[jehovajah]

You didn't read the last post, did you? I already added it myself

Just as I was about to post, I saw the video frame! But my comment still stands as a reply to your original question. lol!

[kram1032]

Another free book on the topic
http://www.math.harvard.edu/~eriehl/cathtpy.pdf
Didn't look much into it yet though.

[kram1032]

What appears to be the first part of a series of books which try to introduce HoTT in a simpler manner http://philsci-archive.pitt.edu/11157/1/HTT_Primer-PART-1.pdf