<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>On 2019-02-07 3:45 a.m., Andrew Pitts wrote:<br>
</p>
<blockquote type="cite"
cite="mid:208DC8C3-C2EA-4192-A028-4F4933F1A62B@cl.cam.ac.uk">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<br class="">
<div>
<blockquote type="cite" class="">
<div class="">On 6 Feb 2019, at 22:06, Jacques Carette <<a
href="mailto:carette@mcmaster.ca" class=""
moz-do-not-send="true">carette@mcmaster.ca</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div class="">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). </div>
</div>
</blockquote>
<div><br class="">
</div>
<div>I guess you were hoping for some way of coding “mere”
existentials in vanilla Agda using its “abstract" or “private”
features.</div>
</div>
</blockquote>
<p>Correct. Or be warned off of trying because there a known
problems...</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:208DC8C3-C2EA-4192-A028-4F4933F1A62B@cl.cam.ac.uk">
<div>
<div> 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 <<a
href="https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/"
class="" moz-do-not-send="true">https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/</a>>).
</div>
</div>
</blockquote>
<p>Just like that. Thanks. <br>
</p>
<p>Though I do think that the following 'trick' does work:</p>
<p>module Hide where<br>
private<br>
data ReallyHidden {ℓ : Level} : Set (suc ℓ) where<br>
box : (C : Set ℓ) → ReallyHidden {ℓ}<br>
<br>
Hidden : {ℓ : Level} → Set (suc ℓ)<br>
Hidden = ReallyHidden<br>
hide : {ℓ : Level} → Set ℓ → Hidden<br>
hide C = box C<br>
</p>
<p>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'.</p>
<p>Of course, to use the above, one most also define an
'existential' record in the same Hide module.</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:208DC8C3-C2EA-4192-A028-4F4933F1A62B@cl.cam.ac.uk">
<div>
<div>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.</div>
</div>
</blockquote>
<p>I'll try that too. Can you recommend some Agda code that
'postulates quotients' that I may learn from?</p>
<p>Jacques<br>
</p>
</body>
</html>