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