MLTT は型の等しさは本当はむしろ入れたくなかったんじゃないのという感じもあるけどなあ。等しさが分裂してる時点で、"no entity without equality" の思想かは怪しいんじゃないか