<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>Hi,</p>
    <p>Yes, you should read Atkey, Ghani and Johann's paper. It's really
      nice, and they prove strictly more than <br>
      Derek and I did. <br>
    </p>
    <p>Best,<br>
      Neel<br>
    </p>
    <div class="moz-cite-prefix">On 07/02/2019 10:33, Andreas Nuyts
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:91b6391a-dda1-e859-dd9e-f3aa3ffb98cb@cs.kuleuven.be">Correction:
      I think Krishnaswami & Dreyer only prove some corrolaries of
      the given theorem.
      <br>
      <br>
      On 7/02/19 11:28, Andreas Nuyts wrote:
      <br>
      <blockquote type="cite">Dear Jacques,
        <br>
        <br>
        You seem to suggest that the first component of your dependent
        pairs is going to be a type. Thus, it seems to me that what you
        are looking for is a parametric existential quantifier, as
        exists in System F, Fω, Haskell, ...
        <br>
        <br>
        Parametric quantification is certainly not available in vanilla
        MLTT/Agda, but is implemented in an experimental branch of agda,
        called agda-parametric:
        <br>
        * github branch: <a class="moz-txt-link-freetext" href="https://github.com/agda/agda/tree/parametric">https://github.com/agda/agda/tree/parametric</a>
        <br>
        * example code: <a class="moz-txt-link-freetext" href="https://github.com/Saizan/parametric-demo">https://github.com/Saizan/parametric-demo</a>
        <br>
        * corresponding paper: "Parametric Quantifiers for Dependent
        Type Theory", ICFP 2017, <a class="moz-txt-link-freetext" href="https://doi.org/10.1145/3110276">https://doi.org/10.1145/3110276</a>
        <br>
        I emphasize that - as far as I understand - the Agda
        implementation (by Andrea Vezzosi) is purely for research and
        there are currently no plans for continued support or
        integration in the master branch.
        <br>
        <br>
        If you want to use vanilla MLTT/Agda, then the following theorem
        may come in handy:
        <br>
        <br>
            Any function in MLTT with small codomain, is parametric.
        <br>
        <br>
        <br>
        (Some papers claim that ANY function in MLTT is parametric; this
        is true for a weaker definition of parametricity that is called
        continuity in our ICFP paper cited above, and that seems
        insufficient for your purposes.)
        <br>
        <br>
        What this boils down to is that any function of type
        <br>
        (p : ∑[ X \in Set ] P X) -> ... -> T,
        <br>
        where T : Set 0, will satisfy the property you are looking for:
        its output does not depend on the first component of p.
        <br>
        <br>
        This is proven metatheoretically in:
        <br>
        Atkey, Ghani, Johann, 2014, "A Relationally Parametric Model of
        Dependent Type Theory."
        <br>
        Krishnaswami & Dreyer, 2013, "Internalizing Relational
        Parametricity in the Extensional Calculusof Constructions",
        <br>
        Takeuti, 2001, "The Theory of Parametricity in Lambda Cube."
        <br>
        <br>
        The theorem breaks down if you add axioms such as
        (non-exhaustively):
        <br>
        * choice / law of excluded middle: (X : Set) -> X + (X ->
        False)
        <br>
        * resizing axioms
        <br>
        <br>
        Best regards,
        <br>
        Andreas
        <br>
        <br>
        On 6/02/19 22:30, Jacques Carette wrote:
        <br>
        <blockquote type="cite">Is there a way to encode an existential
          in Agda where the "exists" part of the dependent pair is
          abstract/private?  ∃ from the standard library just says that
          the first part is implicit (i.e. can be uniquely inferred).
          <br>
          <br>
          I think I could use the same trick as in Haskell (i.e. use a
          wrapper where I don't export the constructor but do provide
          accessor functions that don't leak), but that somehow seems
          heavy.  Is there something simpler?
          <br>
          <br>
          I don't mean a fully non-constructive exists here: I mean
          (informally!) "a dependent pair where the first projection is
          abstract and cannot leak". So to build such a thing, a
          definite type must be used, but once it is created, the
          'clients' as it were, cannot find out what that type is.
          <br>
          <br>
          Jacques
          <br>
          <br>
          _______________________________________________
          <br>
          Agda mailing list
          <br>
          <a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
          <br>
          <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
          <br>
          <br>
        </blockquote>
        <br>
      </blockquote>
      <br>
      <br>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <pre class="moz-signature" cols="72">-- 
Neel Krishnaswami
<a class="moz-txt-link-abbreviated" href="mailto:nk480@cl.cam.ac.uk">nk480@cl.cam.ac.uk</a></pre>
  </body>
</html>