ハイパードクトリン
ハイパードクトリン(hyperdoctrine)
述語論理を依存型理論で圏論的形式化をしたもの?
一階述語論理 ⇆ ハイパードクトリン$ ^{(1)(2)} とのこと
William Lawvereと関係がある
おそらくLogical Relation as Category的な立場な気がする
キーワード: 局所デカルト閉圏
確認用
Q. ハイパードクトリン
関連
カリー＝ハワード対応
カリー／ハワード／ランベック対応
型と論理
参考
(1) relation between type theory and category theory in nLab
(2) Robert A. G. Seely, Hyperdoctrines, Natural Deduction and the Beck Condition, Zeitschr. f. math Logik und Grundlagen d. Math. 29 (1983) 505-542 (pdf)
最近の型理論： 依存型理論で述語論理が出来てしまう理由 - 檜山正幸のキマイラ飼育記 (はてなBlog)
hyperdoctrine in nLab
William Lawvere - Wikipedia
述語論理： 二重圏的ハイパードクトリン - 檜山正幸のキマイラ飼育記 (はてなBlog)
Lars Birkedal, Aleš Bizjak. A Taste of Categorical Logic — Tutorial Notes. 2017-07-10. pdf
調査用
/pogi-log/Google.icon ハイパードクトリン
/pogi-log/Google.icon hyperdoctorine
/pogi-log/Wikipedia.icon
ハイパードクトリン - Wikipedia(日)
ハイパードクトリン(検索) - Wikipedia(日)
/pogi-log/Wikipedia.icon
hyperdctrine - Wikipedia(英)
hyperdoctrine(検索) - Wikipedia(英)