[Agda] Does Agda have this axiom?

[千里冰封]

Greetings,


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`):


open import lib.Basics


variable i : ULevel


test : {A B : Type i} (a : A) (P Q : (A -> B)) -> P a == Q a -> P == Q
test a P Q q = {!!}



------------------
Regards,
ice1000
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181111/4eb29b5b/attachment.html>