GS Chandy
Posts:
8,257
From:
Hyderabad, Mumbai/Bangalore, India
Registered:
9/29/05


Re: Structured Programming
Posted:
Mar 11, 2014 4:42 PM


Many thanks, Joe Niederberger, for drawing our attention to 'Homotopy Type Theory' (HOTT; in your post dt. Mar 4, 2014 1:36 AM [http://mathforum.org/kb/message.jspa?messageID=9400390]) and to the BIG book on it: "Homotopy Type Theory: Univalent Foundations of Mathematics".
I have since reread, quite carefully, the Introduction to the book  No, I've not yet done any modeling there, because I believe this will be possible only when I've at least started studying 'Foundations'. I HAVE made a fair start on 'reading through' "Foundations"  Type Theory; Type Theory Vs. Set Theory; Function Types; Category Theory; etc, etc. (I recall, from my grad school days, that Category Theory used those days to be considered to be a most abstract and perhaps a most advanced topic!!)
I've also read (and listened to) the talk on "Univalent Foundations" by Vladimir Voevodsky.
As noted in an earlier post, some of it is pretty hairy stuff (in particular when I look at some of the 'exercises' in the book). I'm also sure I'll not succeed in 'studying HOTT as a discipline' (with modeling) UNLESS I am guided by someone who's reasonably expert with HOTT. Let's see how it goes.
I believe that the real impact of HOTT will not be just to enable "all mathematicians routinely do all their work in machine readable form and work collaboratively off github. Russel' dream realizedm etc, etc"... I believe HOTT's real impact will be to enhance the 'development of the foundations of math' (much more than is possible by earlier approaches), AND also to help enable people at large (Mr John Doe and Ms Mary Doe) to appreciate and understand AND use math much more effectively than they have been able to do in the past. As I've earlier tried to make clear, this is precisely what OPMS tries to do  perhaps I may be able to interest some HOTT person in this kind of thing as a worthwhile thing to do? Let's see.
However, I DO believe that the 'structures' (the 'higherlevel models') within OPMS would help clarify several of the issues in HOTT. Hopefully, I shall be able to convince someone accordingly at 'The Univalent Foundations Program'. As noted, let's see how it goes.
GSC
Message was edited by: GS Chandy

