[Agda] Abstract existential ?

[Jacques Carette]

On 2019-02-07 3:45 a.m., Andrew Pitts wrote:

>
>> On 6 Feb 2019, at 22:06, Jacques Carette <carette at mcmaster.ca 
>> <mailto: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.

Correct. Or be warned off of trying because there a known problems...


> 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/>). 
>

Just like that. Thanks.

Though I do think that the following 'trick' does work:

module Hide where
   private
     data ReallyHidden {ℓ : Level} : Set (suc ℓ) where
       box : (C : Set ℓ) → ReallyHidden {ℓ}

   Hidden : {ℓ : Level} → Set (suc ℓ)
   Hidden = ReallyHidden
   hide : {ℓ : Level} → Set ℓ → Hidden
   hide C = box C

The problem with the interval is that there are indeed 2 things that 
Agda can see as different. Here, we're using the plain old Haskell trick 
to encode existentials via a 'newtype'.

Of course, to use the above, one most also define an 'existential' 
record in the same Hide module.


> 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.

I'll try that too. Can you recommend some Agda code that 'postulates 
quotients' that I may learn from?

Jacques

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