グロタンディーク同値とパラメータ付き型インスタンス

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

グロタンディーク同値は、

• 忘却ファイブレーション ←→ パラメータ・インデキシング

それに伴って、

• 想起関手 ←→ インデックス付き対象

想起関手は、忘却関手のセクション関手（または部分関手）。インデックス付き対象は、インデキシング圏からの圏論的コンストラクタで、各対象にその対象の圏の対象を割り当てる対応。インデックス付き対象は、パラメータ付き型クラスの依存・型インスタンス、またはパラメータ付き型インスタンスと言える。