Further GSC'S post dt. Mar 12, 2014 2:12 AM (http://mathforum.org/kb/message.jspa?messageID=9410148), some clarifications (which I'd believed would be 'minor' but which I now feel will turn out to be quite the opposite! 'Systems' often (seem to) behave in highly counter-intuitive ways - but Warfield's work has demonstrated that our 'intuitions' are most important for the understanding as well as the design of systems!!!): > > Many thanks, Joe Niederberger, for drawing our <snip> > > I believe that the real impact of HOTT (Homotopy Type > Theory) 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. > <snip> If my surmise above turns out to be correct, it would be remarkable indeed how very advanced work primarily intended to enable
> "all mathematicians routinely do all their work in > machine readable form and work collaboratively off > github. Russel' dream realized" ...
turned out to be the 'engine' that enables significicant 'enhancement of understanding of math concepts by learners' - something that would help overcome the major deficiency in our educational systems that leads to a great many of our students being 'totally turned off' math by the time they pass out of school.
I had long believed that 'Category Theory' would be fundamental in helping make math 'more accessible', so to speak' - but I had no idea just HOW this could come about: I believe HOTT might help significantly. 'Category Theory' is of course (I believe) INCLUDED IN Homotopy Type Theory.
By the way, the relationship "INCLUDES" is 'transitive' and is a most important 'system relationship', in particular in OPMS** (See note).
[**NOTE: Of course, "INCLUDES" is 'transitive' while it is not 'reflexive'. "CONTRIBUTES TO" on the other hand is generally 'transitive' AND 'reflexive'.
[I remark that I had never worked much on "INCLUSIONS" in systems. Though I was fully aware that "INCLUDES" is a most important system relationship, I had been too much occupied in learning (and 'unlearning')'system significance' of "CONTRIBUTES TO" (and its 'negations' "HINDERS" and "PREVENTS" to put much time into the study of "INCLUDES".
[At one stage during the development of the OPMS prototype s/w, a very competent woman mathematician-s/w designer on the ILW team had drawn my attention to the fact that we needed to put in much more effort into understanding "INCLUSIONS". Because of finance and time constraints, we weren't able to put in the needed effort at that time, which in the long run I believe cost us quite dearly.
I now see various structures that seem to imply that some study by myself and my s/w design team of "INCLUSIONS" may well have helped to prevent some of the misunderstandings that led to the closure of Interactive LogicWare (ILW) during the 'dot-com bust'!!
[And, of coure "IMPLIES" is also a very important 'transitive system relationship' that is vastly more difficult to understand than "INCLUDES"...We humans know extremely little about "IMPLIES" - for instance, what may be the IMPLICATIONS (for the human race) of the fact that the USA, which is surely a world leader in 'democratic systems' promotes extremely undemocratic structures in so many of its client nations? The arrival of Obama as POTUS does not seem to have made much of a difference].
To revert to HOTT:
I do believe that the fuller development of HOTT may well help resolve ("LEAD TO resolution of") many of the above 'complexities in our societal systems'.