Incorrect claim of requiring function extensionality

[potato4444]

The book claims that η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f requires function extensionality in the connectives chapter.

plfa.github.io/src/plfa/Connectives.lagda

Line 568 in fccd45a

Elimination followed by introduction is the identity.

But this is not the case. λ x -> f x is judgementally equal to f. This code shows the proof does not require function extensionality:

 η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
 η-→ {A} {B} f = refl

[wadler]

Thank you, fixed! -- P . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ Too brief? Here's why: http://www.emailcharter.org/

On 25 July 2018 at 02:17, potato4444 ***@***.***> wrote: The book claims that η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f requires function extensionality in the connectives chapter. https://github.com/plfa/plfa.github.io/blob/fccd45a05f4e4e2a684792b132599f e0e11e1ea1/src/plfa/Connectives.lagda#L568 But this is not the case. λ x -> f x is judgementally equal to f. This code shows the proof does not require function extensionality: η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f η-→ {A} {B} f = refl — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#41>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEqfsp8LriPyAee3nYs9oolKxUwwFR61ks5uJ7kfgaJpZM4VfPMV> .

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.