[Agda] Is bottom initial without functional extensionality?

[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

On Tue, Mar 27, 2018 at 1:15 AM, Dan Krejsa <dan.krejsa at gmail.com> wrote:

> 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
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180327/8003639c/attachment.html>