<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
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>
<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">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>
</body>
</html>