<div dir="ltr"><div><div>Hi,<br><br>It turns out that if we postulate function extensionality, we can derive bottom using absurd patterns as follows:<br><br>open import Relation.Binary.PropositionalEquality<br>open import Data.Empty<br><br>data T : Set where<br>  c0 : ⊥ → T<br>  c1 : ⊥ → T<br><br>c0≠c1 : c0 ≡ c1 → ⊥<br>c0≠c1 ()<br><br>postulate<br>  fun-ext : {A B : Set} → (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g<br><br>c0=c1 : c0 ≡ c1<br>c0=c1 = fun-ext c0 c1 (λ ())<br><br>wrong : ⊥<br>wrong = c0≠c1 c0=c1<br><br></div>Cheers,<br></div>Gabe<br><br></div>