ハイパードクトリン
ハイパードクトリン(hyperdoctrine)
一階述語論理を依存型理論で圏論的形式化をしたもの?
一階述語論理 ⇆ ハイパードクトリン$ ^{(1)(2)} の対応があること
William Lawvereと関係がある
おそらくLogical Relation as Category的な立場な気がする
キーワード: 局所デカルト閉圏
確認用
Q. ハイパードクトリン
関連
カリー＝ハワード対応
カリー／ハワード／ランベック対応
型と論理
型と圏論
Categorical Logic
参考
(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
メモ
米田 豊
An Introduction to Hyperdoctrines - Google ドライブ
調査用
/pogi-log/Google.icon ハイパードクトリン
/pogi-log/Google.icon hyperdoctorine
/pogi-log/Wikipedia.icon
ハイパードクトリン - Wikipedia(日)
ハイパードクトリン(検索) - Wikipedia(日)
/pogi-log/Wikipedia.icon
hyperdctrine - Wikipedia(英)
hyperdoctrine(検索) - Wikipedia(英)
#型と論理
#論理と圏論