<div dir="ltr"><div>It's possible to build models of an Agda-like theory that explicitly refute funext (see <a href="https://www.xn--pdrot-bsa.fr/articles/cpp2017.pdf">https://www.pédrot.fr/articles/cpp2017.pdf</a>), 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).<br><br></div>-- Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 27, 2018 at 1:15 AM, Dan Krejsa <span dir="ltr"><<a href="mailto:dan.krejsa@gmail.com" target="_blank">dan.krejsa@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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...<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888">- Dan<br></font></span></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>