本日は集合論・型理論・圏論の相互の翻訳可能性について。 集合論をメタ理論として、集合論の内部に直観主義的高階論理(IHOL)の翻訳を作成することは簡単。はい、いつもの型理論の集合論的モデル（をみたいに翻訳する）です。この翻訳によって定められる集合…

朝から雨、とても寒い。午前は研究集会。午後は京阪線経由で研究所に行き、書類処理や原稿書き、やっと発送した。ついでにメールを8通書いた。