The real numbers in homotopy type theory http://math.andrej.com/2016/06/15/the-real-numbers-in-homotopy-type-theory-cca-2016-slides/ 読んでる。 HoTTやHITって型理論的自体の研究としてはわかるけれど、 普通の数学的対象を形式化するうえでどう嬉しいかあまりピンと来ていなかったので、 コーシー実数を形式化するのに、こう使うんだ、というのが面白かった。