<div dir="ltr">Thank you for your answers.<div><br></div><div>I did not realize that I needed to enable injective type constructors, thanks Andreas for pointing that out. Also I now feel very stupid for the mistake in the equal-types code :$</div>
<div><br></div><div>When you look at the problem from a HoTT perspective (with univalence), then indeed it doesn't seem right to have injectivity of type constructors, or of -> for that matter. I guess I can live with the extra argument to my cong function if it's necessary to bring the magic of HoTT to Agda.</div>
<div><br></div><div>Best regards,</div><div>Jesper</div></div>