忘却ファイブレーション ＝ 指標の分割が定義する、忘却関手を射影関手とするファイブレーション パラメータ・インデキシング ＝ パラメータ付き指標が定義する、パラメータ指標のモデル圏をインデキシング圏とするインデキシング（インデックス付き圏） グ…

指標のあいだの構成〈construction〉は、ML言語のファンクタと同じ概念。引数がない構成がML言語のストラクチャ。問題は、パラメータ付き指標のあいだの構成＝パラメータ付き構成。意味論はむしろ簡単で、パラメータ付き指標の意味がインデックス付き圏だか…

型クラス＝指標の立場なら、指標Σの意味は〚Σ〛 := Mod[Σ]。そのインスタンスは〚Σ〛の対象のこと。実に素直。圏Pに対して、ΣのP-パラメトライズ・インスタンスを P→〚Σ〛と定義する。自明圏Iに対するI-パラメトライズ・インスタンスはインスタンスと同一視…