type of types とかラムダキューブについて教えてもらった。これは面白いネタなので、別エントリ(来年?)にして書くかも。
ラムダキューブについては、稲葉(k.inaba)さんが説明してくださったのですが、その一部 -- 型パラメータを取る型は、デカルト閉圏と豊饒圏(enriched category)を使うとうまく定式化できそうな感じを抱きました。それで、年末年始業務の合間に、「ボブ・クックの『物理系実務者のための圏論入門』」の冒頭で紹介したことがある、Francis BorceuxとIsar Stubbeによる"SHORT INTRODUCTION TO ENRICHED CATEGORIES"(http://www.win.ua.ac.be/~istubbe/PDF/EnrichedCatsKLUWER.pdf)という論説を読み返していました。
そしたら、閉圏や豊饒圏の実例をいじるのがなんか楽しくなってしまいましたよ。「型パラメータを取る型」の話もいずれは書くと思いますが、その前に閉圏/豊饒圏ネタが来そう。