<div dir="ltr"><div>Hi Thorsten,</div><div><br></div><div>That's what I thought at first, but then I realized it would be unsound to have the projections even *without* eta equality, since you would still be able to get something relevant out of a Prop. So it is the existence of the projections itself rather than eta which is problematic for such a type.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jun 5, 2019 at 4:23 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div class="gmail-m_8717696954740718177WordSection1">
<p class="MsoNormal">I would paraphrase tis differently: the eta rule for record times makes the projections strictly injective and this is obviously false in this example. Or do I miss something here?<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thorsten<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div style="border-color:rgb(181,196,223) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Andrew Pitts <<a href="mailto:andrew.pitts@cl.cam.ac.uk" target="_blank">andrew.pitts@cl.cam.ac.uk</a>><br>
<b>Date: </b>Wednesday, 5 June 2019 at 14:45<br>
<b>To: </b>Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>>, agda list <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>Re: [Agda] Prop in Agda 2.6 - again<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">Dear Jesper,<u></u><u></u></p>
<div>
<p class="MsoNormal"><br>
<br>
<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<p class="MsoNormal">On 5 Jun 2019, at 13:34, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:<u></u><u></u></p>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<div>
<p class="MsoNormal">Hi Andy,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">When you define a datatype in Prop, the resulting type is automatically 'squashed', i.e. any two elements are equal. In contrast, for record types this is not possible because then it is impossible to define the projections. For your definition
 of <span style="font-family:"Cambria Math",serif">∃</span> in Prop, (true , _) is equal to (false , _) of type `<span style="font-family:"Cambria Math",serif">∃</span> Bool (λ _ →
<span style="font-family:"Cambria Math",serif">⊤</span>)`, but their first projections are not equal. It would theoretically be possible to have such a record type but not give access to the projections and disabling eta-equality, but then you could've equally
 defined it as a single-constructor datatype.<u></u><u></u></p>
</div>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">I see. So to paraphrase your explanation, Agda imposes a simple syntactic restriction on what record types can be declared to have type Prop in order to maintain the soundness of forcing all elements of an element of a Prop to be definitionally
 equal.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">I can think of a simple syntactic restriction that is less liberal than the current one: don’t allow record types in Prop! Is there an example of why my restriction is too restrictive? —- in other words a case where using a record of Prop
 type is really better than using a corresponding single-constructor datatype of type Prop?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">(I am thinking that one often uses a record type in Set instead of a single-constructor-datatype in Set, in order to get definitional eta expansion; but that’s automatic for elements of Prop, due to the definitional proof irrelevance.)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Andy<u></u><u></u></p>
</div>
<div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal"><br>
<br>
<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">-- Jesper<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Wed, Jun 5, 2019 at 1:09 PM Andrew Pitts <<a href="mailto:andrew.pitts@cl.cam.ac.uk" target="_blank">andrew.pitts@cl.cam.ac.uk</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal">Here is another question about Prop in Agda 2.6. Can anyone enlighten me?<br>
<br>
The documentation says<br>
<br>
"Just as for Set, we can define new types in Prop’s as data or record types”<br>
<br>
However, although Agda 2.6 allows the declaration of the following one-constructor datatype<br>
<br>
data <span style="font-family:"Cambria Math",serif">∃</span> {l m}(A : Set l)(P : A → Prop m) : Prop (l
<span style="font-family:"Cambria Math",serif">⊔</span> m) where<br>
  _,_ : (x : A)(p : P x) → <span style="font-family:"Cambria Math",serif">∃</span> A P<br>
<br>
if instead I try to define a record type<br>
<br>
record <span style="font-family:"Cambria Math",serif">∃</span> {l m : Level}(A : Set l)(B : A → Prop m) : Prop (l
<span style="font-family:"Cambria Math",serif">⊔</span> m) where<br>
  constructor _,_<br>
  field<br>
    fst : A<br>
    snd : B fst<br>
<br>
Agda complains (somewhat ungrammatically) that <br>
<br>
"Set l is not less or equal than Prop (l <span style="font-family:"Cambria Math",serif">
⊔</span> m) when checking the definition of <span style="font-family:"Cambria Math",serif">
∃</span>”<br>
<br>
So it doesn’t mind the parameter (A : Set l) when defining a datatype in Prop (l <span style="font-family:"Cambria Math",serif">
⊔</span> m), but does mind it when defining a record type.<br>
<br>
Why is that?<br>
<br>
Andy<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></p>
</blockquote>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><br>
<br>
<u></u><u></u></p>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.



</pre></div>

</blockquote></div>