univalence を仮定するとすべての関数のグラフが等しくなるので、univalenceと整合的であるIMLTTではそれを否定出来ないし、「グラフの等しい関数は(pointwiseに)等しい」ことも証明できないとか。 面白いけど、なんだかなぁ……
https://lists.chalmers.se/pipermail/agda/2012/003958.html