数学順序問題の話題も出てて、またTaPL読みたくなった＞＜；（オレンジはその問題は型理論で解決できると考えてる＞＜）