In Agda function extensionality can be defined like this:
funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2
One may note a similarity in the definition of a (binary) logical relation
f1 [A -> B] f2 being:
∀ x1 x2 → x1 [A] x2 -> f1 x1 [B] f2 x2.

What is the relation of logical relations to function extensionality? Is there perhaps a relation to eta-equality?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.