<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Correction: I think Krishnaswami & Dreyer only prove some
    corrolaries of the given theorem.<br>
    <br>
    <div class="moz-cite-prefix">On 7/02/19 11:28, Andreas Nuyts wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:3ef4c30a-7561-d969-9201-e7e73e38d3ad@cs.kuleuven.be">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      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"
        moz-do-not-send="true">https://github.com/agda/agda/tree/parametric</a><br>
      * example code: <a class="moz-txt-link-freetext"
        href="https://github.com/Saizan/parametric-demo"
        moz-do-not-send="true">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" moz-do-not-send="true">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>
      <blockquote>Any function in MLTT with small codomain, is
        parametric.<br>
      </blockquote>
      <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, "<span style="left: 76.3802px; top:
        615.668px; font-size: 13.2835px; font-family: sans-serif;
        transform: scaleX(0.888169);">A Relationally Parametric Model of
        Dependent Type Theory.</span>"<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>
      <div class="moz-cite-prefix">On 6/02/19 22:30, Jacques Carette
        wrote:<br>
      </div>
      <blockquote type="cite"
        cite="mid:6bcd3784-b5d8-bc25-f042-09d96021f099@mcmaster.ca">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" moz-do-not-send="true">Agda@lists.chalmers.se</a>
        <br>
        <a class="moz-txt-link-freetext"
          href="https://lists.chalmers.se/mailman/listinfo/agda"
          moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
        <br>
        <br>
      </blockquote>
      <br>
    </blockquote>
    <br>
  </body>
</html>