[Agda] Is bottom initial without functional extensionality?

[Dan Krejsa]

Hi,

If ⊥ is the prototypical empty type, is it possible in Agda to prove

from⊥uniq : ∀ {i} {A : Set i} (f g : ⊥ -> A) -> f ≡ g

(where ≡ is propositional equality) without assuming extra postulates
such as functional extensionality?
My instinct is to doubt it, but the emptiness of the domain gives me
pause...

- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180326/90986669/attachment.html>