Functors as Types とラムダ計算とカン拡張

Sをスキーマとか指標と呼ばれる圏（または圏の表示）として、型は関手圏 [S, C] の対象となる。Sが含まれる圏の圏（ドクトリン）をDとする。

x:S→X in D が部分関手として、E:S→C も部分関手（部分的に定義された、Cに値を取る意味）として、この状況自体を λx.E と表すことができる。別に R:X→C があると、一種のカン拡張として (λx.E)・R を定義できる気がする。