ちょっと読み飛ばしていたが
>>350
>集合族という言葉を使う現代数学は全て型理論を使っている

↑