<div><font face="幼圆" size="2" color="#333333">Greetings,</font></div><div><font face="幼圆" size="2" color="#333333"><br></font></div><div><font face="幼圆" size="2" color="#333333">I wonder if there's some way that allows me to typecheck this (_==_, Type are from HoTT-Agda, which can be replaced  by the builtin equality type and `Set`):</font></div><div><font face="幼圆" size="2" color="#333333"><br></font></div><div><font face="幼圆" size="2" color="#333333"><div>open import lib.Basics</div><div><br></div><div>variable i : ULevel</div><div><br></div><div>test : {A B : Type i} (a : A) (P Q : (A -> B)) -> P a == Q a -> P == Q</div><div>test a P Q q = {!!}</div></font></div><div><font face="幼圆" size="2" color="#333333"><br></font></div><div><div style="color:#909090;font-family:Arial Narrow;font-size:12px">------------------</div><div style="font-size:14px;font-family:Verdana;color:#000;"><div>Regards,</div><div>ice1000</div><div><br></div></div></div><div> </div>