Discussion:
Is bottom initial without functional extensionality?
Add Reply
Dan Krejsa
2018-03-26 23:15:47 UTC
Reply
Permalink
Raw Message
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
2018-03-27 09:09:52 UTC
Reply
Permalink
Raw Message
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
Loading...