この記事内では、「型」と「集合」は同義語です。つまり、sets-as-types の立場をとります*1。集合〈型〉のファミリー〈族〉があったとき、それからシグマ型とパイ型を構成できます。この構成は、次のような写像を与えます。$`\quad \sum, \prod: |{\bf Fam}…