[Agda] Abstract existential ?

[Andrew Pitts]

> On 6 Feb 2019, at 22:06, Jacques Carette <carette at mcmaster.ca> wrote:
> 
> Thanks - I was aware that in HoTT/UF, this was just propositional truncation. And that in cubical Agda, this should just 'work'. But I am trying to get as far as possible with 'vanilla' Agda (without any axioms, for funext is out too). 

I guess you were hoping for some way of coding “mere” existentials in vanilla Agda using its “abstract" or “private” features. However the semantics of those features is not well understood — there have been examples in the past where apparently private information can leak in unexpected ways leading to logical inconsistency (for example the disjointness property of constructors is hard to hide — see the last comment at <https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/ <https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/>>). My own preference would be to restrict to a core of Agda that is vanilla Martin-Löf Type Theory and then postulate an axiom that is known to be consistent with it. Postulating quotients (of the kind provided by default in Lean 3) works nicely and allows one to side-step setoid hell (and as you probably know, implies function extensionality as well). However this approach may not fit what you have in mind to do with Agda.

Andy

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190207/4f42dc03/attachment.html>