[Agda] Does Agda have this axiom?

[Martin Escardo]

I was going to say something similar to Nicolai.

On 14/11/2018 19:14, nicolai.kraus at gmail.com wrote:
> On Wed, Nov 14, 2018 at 6:50 PM 千里冰封 <ice1000kotlin at foxmail.com 
> <mailto:ice1000kotlin at foxmail.com>> wrote:
> 
>     test : {A B : Type i} (a : A) (P Q : (A -> B)) -> P a == Q a -> P == Q

Did you mean

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

Or, in words, if P and Q have equal values, then they are themselves 
equal. This is called function extensionality, as Nicolai said.

This is not provable in Agda, but it is something we all often want. 
Cubical Agda (that is, Agda with the --cubical option), does have that.

A small cubical Agda library (under development) is at 
https://github.com/agda/cubical

But warning: understanding this kind of thing goes much beyond 
understanding dependent type theory, and goes under the names HoTT/UF, 
univalent foundations, univalent mathematics, univalent type theory, 
cubical type theory. Unfortunately, at the moment this is not well 
documented for the casual user.

But the file 
https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agda 
provides an abstraction layer that allows to use, in particular, 
function extensionality, in such a way that it computes (and an example 
is included in that file).

M.

> 
> 
> 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
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe