Universal domain 検索性ゴミやな。まあ普通話題にせんか。その昔、「untype lambda の項に対して型ってどうなるんやろ?」と考えた人がいて、「なんかうまいモデルないかな?せや、λx.x と (λx.x) (λx.x) には型的な違いはないことにしよ。untyped lambda は uni-typed lambda や」で、モデルが上手く作れちゃった話があってなみたいな