型クラスと型インスタンスと意味論:グロタンディーク同値

型クラス=指標の立場なら、指標Σの意味は〚Σ〛 := Mod[Σ]。そのインスタンスは〚Σ〛の対象のこと。実に素直。

圏Pに対して、ΣのP-パラメトライズ・インスタンスを P→〚Σ〛と定義する。自明圏Iに対するI-パラメトライズ・インスタンスインスタンスと同一視できる。

指標ベース忘却関手 U = UΔ≦Σ〚(Σ = Δ +> Σ')〛→〚Δ〛 があるとき、Uのセクション関手は〚Δ〛→〚Σ〛 になる。忘却関手(忘却ファイブレーション)のセクションはパラメトリック多相の意味の“パラメトリックインスタンス”。〚Δ〛の部分圏で定義された部分セクションはアドホック多相の意味の“アドホックインスタンス”。インスタンスと言っているが、実体は関手である。

「指標の分割 ←→ 指標のパラメータ化」に対応して「忘却ファイブレーション ←→ インデックス付き圏」の対応が作れる。後者の同値性はグロタンディーク同値

忘却ファイブレーションの部分セクションは想起関手〈recollection functor〉