HoTT, первые впечатления

Больше для себя, зафиксировать, предыстория здесь и здесь.

Прочитал первые четыре главы http://hottheory.files.wordpress.com/2013/03/hott-a4.pdf.  Первые две главы прочитал уже на два раза. Страниц там 475, а не 600.

Дальше много про математику, довольно нудно. В конце вывод о классах программ, для которых можно строго доказать вычислимость.

( Read more... )