デカルト閉圏(CCC)

デカルト閉圏(デカルトへいけん、Cartesian Close Category(CCC))

プログラミング言語はデカルト閉圏と言えるらしい。

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

圏$ C がデカルト閉である条件は

$ C が終対象を持つ

$ C の任意の二対象$ X, Y に対し、C はそれらの直積$ X × Y を対象に持つ

$ C の任意の二対象$ Y, Z に対し、$ C はそれらの冪対象$ Z^Y を対象に持つ。

圏論的に考えると

型が対象

関数が射

関数合成が射の合成

id関数が恒等射

確認用

Q. デカルト閉圏とは

関連

参考

デカルト閉圏とその応用（1/3）... 概要 - YouTube

https://www.youtube.com/watch?v=en7Y0aYvza4

デカルト閉圏とその応用（2A/3）... デカルト閉圏の基礎その１積，極限，和，余極限の復習 - YouTube

https://www.youtube.com/watch?v=zkZIWTDkXwE

デカルト閉圏とその応用（2B/3）... デカルト閉圏の基礎その２冪（べき）とデカルト閉圏 - YouTube

https://www.youtube.com/watch?v=3CvHDVvOWi0

カルテジアン閉圏とは，ひとことで言うと，有限直積(finite products)と冪(exponentials)を持つ圏です．

メモ