CCC

Cartesian Closed Category ですね。名前からしてかっこいいじゃないですか。

　　Hom A a 1 ≅ {*}
　　Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
　　Hom A a (c ^ b) ≅ Hom A (a × b) c

とか書いてあるな。これって何? ってあたりからやるようです。

いや、先にやること他にあるはずなんだけど。

たぶん、これが型付きλ計算のモデルになるとかやるはずだな。M2の時にもλ計算の分厚い本で読んだような気がするが、あの時は良くわかってなかったな。