[Agda] Does Agda have this axiom?

[Nicolai Kraus]

On Wed, Nov 14, 2018 at 6:50 PM 千里冰封 <ice1000kotlin at foxmail.com> wrote:

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

P and Q are functions A -> B, but you only know that they are equal for one
single input a:A. The functions could differ for other inputs, so you
should not expect that they are equal.
Maybe you want to look up "function extensionality" (which looks similar
but says something very different).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181114/bb9b6287/attachment.html>