[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

[Nicolai Kraus]

Post by 千里冰封
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).

[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

Post by Nicolai Kraus

Post by 千里冰封
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
https://lists.chalmers.se/mailman/listinfo/agda

[Martin Escardo]

I was going to say something similar to Nicolai.

Post by 千里冰封
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.

Post by 千里冰封
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
https://lists.chalmers.se/mailman/listinfo/agda