別に全称・存在量化を依存型で見るのは Martin-Löf に始まったことではないと思うけど、それをプリミティブに置く哲学的正当性みたいなのを気にしているのか

BHK したらそうなったじゃダメなのかしら

Martin-Löf は definitional equality と judgemental equality を区別しているのか

W-type なにもわからないの良くない気がしてきた

MLTT は型の等しさは本当はむしろ入れたくなかったんじゃないのという感じもあるけどなあ。等しさが分裂してる時点で、"no entity without equality" の思想かは怪しいんじゃないか

だからこそ HOTT に興味がある

Brouwer 的な等しさの概念は MLTT / HoTT では完全にキャプチャーできてないと思うんだよなあ

でもいろいろ突っ込みたくなる授業はいい授業なのかもしれない

いろいろ突っ込みたくなるのを抑えている

えー……