まず、Leanコミュニティでも用語の個人差がある。object, term, value, element なんかは要注意。
型クラスのパラメータは、相対指標の部分指標の指定なので、ファイバー付き圏のベース圏を指定する。C が1パラメータの型クラスとして、固定したξに対して (C ξ) はファイバー付き圏のファイバー（である圏）を表す。(C ξ)が型インスタンスだというのは嘘、ないしは方便。
EがCのインスタンスのとき、(E α) のαを動かしてまたファイバー付き圏を作れる。インスタンスとは、ファイバー付き圏のあいだの射。特に、自明ファイバー付き圏からの射は大域セクションになる。通常、大域セクションは期待できないので部分セクション。
セクションとは、ファイブレーションの大域ポイントのこと。自明ファイブレーションをシングルトンと呼ぶ。サブシングルトンとは、ファイブレーションの圏におけるシングルトンのサブオブジェクトのこと。サブシングルトンからのファイブレーションの射はサブポイントになる。
というわけで、型クラスの型インスタンスとは、与えられたファイブレーションのサブポイントのことが多い。バンドルの言葉で言えば、ローカルセクション。
