[Agda] Does Agda have this axiom?

[Apostolis Xekoukoulotakis]

Have a look at cubical.

funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
funExt p = λ i x → p x i


https://github.com/agda/cubical/blob/43bba3614117b6b107787c137f5776af2e128710/Cubical/Core/Prelude.agda#L79

On Wed, Nov 14, 2018 at 9:14 PM Nicolai Kraus <nicolai.kraus at gmail.com>
wrote:

> 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).
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181114/b0e92518/attachment.html>