トップ «前の日記(2008-07-28) 最新 次の日記(2008-08-01)» 月表示 編集

日々の流転


2008-07-31 [長年日記]

λ. 依存型とcatamorphism

Agda2ことはじめ - ラシウラ の記述を読んで、そういえば依存型を用いた除去規則って、(弱)始代数の普遍性とはどう関係するんだろうか、と思ったので、category with attributes で考えてみた……んだけど、書いてたら混乱してきたので、何回かに分けて書くことにする。

  1. Categories with attributes (cwa)
  2. cwaでのユニット型の解釈