[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

[Jesper Cockx]

It's possible to build models of an Agda-like theory that explicitly refute
funext (see https://www.pédrot.fr/articles/cpp2017.pdf
<https://www.xn--pdrot-bsa.fr/articles/cpp2017.pdf>), and this seems like
it could be specialized to the case where the domain is the empty type. So
I would strongly doubt this is provable in Agda (without exploiting some
kind of bug).

-- Jesper

Post by 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
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda