Унивалентные основания математики
Вот страничка материалов про унивалентные основания математики Владимира Воеводского: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html -- язык Coq, классы не как sets, а как homotopy types, теория категорий. Далее -- Eventually it became clear to me that the univalent semantics is just a first step and that I am really working on new foundations of mathematics.
Меня чем дальше, тем больше интересуют подходы к классам, в которых они не являются множествами. Связанный с этим парадокс -- что простые смертные классами-не-множествами как раз и думают (http://ailev.livejournal.com/1007293.html), но предлагаемые математикой и компьютерной наукой формализмы этих "не-множеств" простым смертным недоступны.
Меня чем дальше, тем больше интересуют подходы к классам, в которых они не являются множествами. Связанный с этим парадокс -- что простые смертные классами-не-множествами как раз и думают (http://ailev.livejournal.com/1007293.html), но предлагаемые математикой и компьютерной наукой формализмы этих "не-множеств" простым смертным недоступны.