{"action":"created","issue":{"url":"https://api.github.com/repos/plfa/plfa.github.io/issues/41","repository_url":"https://api.github.com/repos/plfa/plfa.github.io","labels_url":"https://api.github.com/repos/plfa/plfa.github.io/issues/41/labels{/name}","comments_url":"https://api.github.com/repos/plfa/plfa.github.io/issues/41/comments","events_url":"https://api.github.com/repos/plfa/plfa.github.io/issues/41/events","html_url":"https://github.com/plfa/plfa.github.io/issues/41","id":344247409,"node_id":"MDU6SXNzdWUzNDQyNDc0MDk=","number":41,"title":"Incorrect claim of requiring function extensionality","user":{"login":"potato4444","id":32945005,"node_id":"MDQ6VXNlcjMyOTQ1MDA1","avatar_url":"https://avatars3.githubusercontent.com/u/32945005?v=4","gravatar_id":"","url":"https://api.github.com/users/potato4444","html_url":"https://github.com/potato4444","followers_url":"https://api.github.com/users/potato4444/followers","following_url":"https://api.github.com/users/potato4444/following{/other_user}","gists_url":"https://api.github.com/users/potato4444/gists{/gist_id}","starred_url":"https://api.github.com/users/potato4444/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/potato4444/subscriptions","organizations_url":"https://api.github.com/users/potato4444/orgs","repos_url":"https://api.github.com/users/potato4444/repos","events_url":"https://api.github.com/users/potato4444/events{/privacy}","received_events_url":"https://api.github.com/users/potato4444/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-07-25T00:17:34Z","updated_at":"2018-07-25T08:14:23Z","closed_at":null,"author_association":"NONE","body":"The book claims that `η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f` requires function extensionality in the connectives chapter.\r\n\r\nhttps://github.com/plfa/plfa.github.io/blob/fccd45a05f4e4e2a684792b132599fe0e11e1ea1/src/plfa/Connectives.lagda#L568\r\n\r\nBut this is not the case. `λ x -> f x` is judgementally equal to `f`. This code shows the proof does not require function extensionality:\r\n\r\n     η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f\r\n     η-→ {A} {B} f = refl"},"comment":{"url":"https://api.github.com/repos/plfa/plfa.github.io/issues/comments/407672373","html_url":"https://github.com/plfa/plfa.github.io/issues/41#issuecomment-407672373","issue_url":"https://api.github.com/repos/plfa/plfa.github.io/issues/41","id":407672373,"node_id":"MDEyOklzc3VlQ29tbWVudDQwNzY3MjM3Mw==","user":{"login":"wadler","id":4890546,"node_id":"MDQ6VXNlcjQ4OTA1NDY=","avatar_url":"https://avatars3.githubusercontent.com/u/4890546?v=4","gravatar_id":"","url":"https://api.github.com/users/wadler","html_url":"https://github.com/wadler","followers_url":"https://api.github.com/users/wadler/followers","following_url":"https://api.github.com/users/wadler/following{/other_user}","gists_url":"https://api.github.com/users/wadler/gists{/gist_id}","starred_url":"https://api.github.com/users/wadler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wadler/subscriptions","organizations_url":"https://api.github.com/users/wadler/orgs","repos_url":"https://api.github.com/users/wadler/repos","events_url":"https://api.github.com/users/wadler/events{/privacy}","received_events_url":"https://api.github.com/users/wadler/received_events","type":"User","site_admin":false},"created_at":"2018-07-25T08:14:22Z","updated_at":"2018-07-25T08:14:22Z","author_association":"COLLABORATOR","body":"Thank you, fixed! -- P\n\n.   \\ Philip Wadler, Professor of Theoretical Computer Science,\n.   /\\ School of Informatics, University of Edinburgh\n.  /  \\ and Senior Research Fellow, IOHK\n. http://homepages.inf.ed.ac.uk/wadler/\n\nToo brief? Here's why: http://www.emailcharter.org/\n\nOn 25 July 2018 at 02:17, potato4444 <notifications@github.com> wrote:\n\n> The book claims that η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x)\n> ≡ f requires function extensionality in the connectives chapter.\n>\n> https://github.com/plfa/plfa.github.io/blob/fccd45a05f4e4e2a684792b132599f\n> e0e11e1ea1/src/plfa/Connectives.lagda#L568\n>\n> But this is not the case. λ x -> f x is judgementally equal to f. This\n> code shows the proof does not require function extensionality:\n>\n>  η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f\n>  η-→ {A} {B} f = refl\n>\n> —\n> You are receiving this because you are subscribed to this thread.\n> Reply to this email directly, view it on GitHub\n> <https://github.com/plfa/plfa.github.io/issues/41>, or mute the thread\n> <https://github.com/notifications/unsubscribe-auth/AEqfsp8LriPyAee3nYs9oolKxUwwFR61ks5uJ7kfgaJpZM4VfPMV>\n> .\n>\n\nThe University of Edinburgh is a charitable body, registered in\nScotland, with registration number SC005336.\n"}}
{"actor":{"display_login":"wadler"}}