http://return0.info/note/2011-01-30.e : ライブラリを分離してリリースとなると、やっぱ一番ホットに感じてるところから離れた気がするのがなあ。 この気分は僕も同じ。説明しやすくて皆んなに役に立ちそうな部分ってのがあって、それの意義は認識している…

圏の指数の書き方は、含意記号「⊃」を使うことにします。デカルト閉圏は、型付きラムダ計算や連言含意論理のモデルなので、いくらでも例を作れます。非自明で最も簡単な例は、二値の真偽値を圏とみなしたモノでしょう。この例はやたらに簡単なので、手作業で…