型と圏論

沼すぎてさっぱりである

table:型理論と圏論

型理論 圏論

型(type) 対象(object)

一般化された要素 項(term)/プログラム(program)

(generalized element)

空型(empty type) 始対象(initial object)

単純型付きラムダ計算 デカルト閉圏

(よくわかってない概念は記載できていない)

型と対象

型理論の型は、圏論の対象と対応する

関連

参考

メモ

[1] T. Zhang, “Type theories in category theory,” Apr. 04, 2022, arXiv: arXiv:2107.13242. doi: 10.48550/arXiv.2107.13242.