別に全称・存在量化を依存型で見るのは Martin-Löf に始まったことではないと思うけど、それをプリミティブに置く哲学的正当性みたいなのを気にしているのか