マルティン＝レーフが彼の哲学に基づいて型理論を提案した本は
確かに数学的にはトリビアルな内容しかない。
その後彼の型理論が計算機科学や証明論の研究対象になったが
そういう研究がトリビアルと言える程に俺は頭よくない。
証明論的にヒュームの原理を分析しているWalshの論文も
同様だろうと断定的にはいえないがそうだと推測する。