higher-order logic topos で検索すると 高名な 下記のSteve Awodey先生がヒット Kohei Kishida Who? ” sheaf semantics, models are built on presheaves ” なるほど、層や圏から、higher-order logicへ繋がっていくのか（＾＾
参考 https://arxiv.org/pdf/1403.0020.pdf Topos Semantics for Higher-Order Modal Logic March 4, 2014 Steve Awodey? Kohei Kishida† Hans-Christoph Kotzsch‡ †Department of Computer Science, University of Oxford (抜粋) Abstract. We define the notion of a model of higher-order modal logic in an arbitrary elementary topos E. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the subobject classifier ΩE , but rather by a suitable complete Heyting algebra H. The canonical map relating H and
