全称限量子とタプル

(X∋x P_x) がパラメトライズ（インデックス、パラメトリック）族だとする。これを全称束縛すると、∀x∈X.P_x となるが、これは タプル 〈P_x〉_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 単一の証明

もっと考えないと。