<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&#39;t seem right to have injectivity of type constructors, or of -&gt; for that matter. I guess I can live with the extra argument to my cong function if it&#39;s necessary to bring the magic of HoTT to Agda.</div>

<div><br></div><div>Best regards,</div><div>Jesper</div></div>