Интересная презентация -- http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf via http://mathoverflow.net/questions/176372/proof-correctness-problem