\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(B:A\to \mathcal {U}(i)\)を\(A\)上の型の族(type family)と呼ぶ。