[Agda] Absurd patterns inconsistent with function extensionality

[Gabe Dijkstra]

Hi,

It turns out that if we postulate function extensionality, we can derive
bottom using absurd patterns as follows:

open import Relation.Binary.PropositionalEquality
open import Data.Empty

data T : Set where
  c0 : ⊥ → T
  c1 : ⊥ → T

c0≠c1 : c0 ≡ c1 → ⊥
c0≠c1 ()

postulate
  fun-ext : {A B : Set} → (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g

c0=c1 : c0 ≡ c1
c0=c1 = fun-ext c0 c1 (λ ())

wrong : ⊥
wrong = c0≠c1 c0=c1

Cheers,
Gabe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150501/7e170f06/attachment.html