実は Agda の上で impredicative な議論が強力に展開できるということ、そして証明論的にはアホみたいに強いということ。驚きました。

残暑。長袖シャツを脱いでTシャツで過ごす。 8時15分に起床、阪急駅前でサンドイッチと紅茶で朝食、出勤して論文読み。昼はカキフライ弁当、奮発して付け合わせにサバと秋なすの香味揚げを食べる。午後は研究打ち合わせ。 18時にKTさんと議論を始め、気がつ…