On 19/11/2018 20.18, Guillaume Brunerie wrote: > Of course in that case they are both (propositionally) equal, that’s > why a mathematician is happy with it, but which one should Agda > choose? A design choice of Agda is, roughly speaking, to never make an unforced choice. -- /NAD