<div dir="ltr"><div><div><div><div><div><div>Hi,<br><br></div>If ⊥ is the prototypical empty type, is it possible in Agda to prove<br><br></div>from⊥uniq : ∀ {i} {A : Set i} (f g : ⊥ -> A) -> f ≡ g<br><br></div><div>(where ≡ is propositional equality) without assuming extra postulates<br>such as functional extensionality?<br></div></div>My instinct is to doubt it, but the emptiness of the domain gives me pause...<br></div><br></div>- Dan<br></div>