型と圏論
沼すぎてさっぱりである
カリー／ハワード／ランベック対応
だと型理論、論理、圏論までの対応がある
Homotopy Type Theory(HoTT)
だと広いもっと広い対応がある？
table:型理論と圏論
型理論 圏論
型 対象
empty type 始対象
product type 積
sum type 余積
単位型
(
unit type
)h-level 0-type 終対象/(-2)-truncated object
積型(
パイ型
、
依存積型
)
積
和型(sum type)、
依存和型
余積
関連
モナド
デカルト閉圏(CCC)
参考
https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory
メモ
依存型理論の圏論的セマンティクスの資料 - 檜山正幸のキマイラ飼育記 (はてなBlog)
『Homotopy Type Theory Univalent Foundations of Mathematics』Chapter 9 Category theory
[1] T. Zhang, “Type theories in category theory,” Apr. 04, 2022, arXiv: arXiv:2107.13242. doi: 10.48550/arXiv.2107.13242.
http://arxiv.org/abs/2107.13242
#依存型理論
#圏論