agda-list の Unification assumes injective postulates? というスレッド https://lists.chalmers.se/pipermail/agda/2012/thread.html#4673 が面白い。 postulateの解釈についてuniversalな解釈とexistentialな解釈が考えられるという話で、自分はどちらを意図して使ったこともあったけれど、その違いについて気づいた＆考えたことはなかったなぁ……