(X∋x Px) がパラメトライズ(インデックス、パラメトリック)族だとする。これを全称束縛すると、∀x∈X.Px となるが、これは タプル 〈Px〉x∈X と書いても同じ。
x∈X. Px 命題族 -------------------- ∀x∈X.Px 単一命題
x∈X. Px 型族 ------------------- Π(Px)x∈X 単一の型
x∈X. fx: x → Px 証明族 ------------------------------------ 〈fx〉x∈X:T → Π(Px)x∈X 単一の証明
もっと考えないと。