<div dir="ltr">Michel,<div><br></div><div>Questions like your are welcome on <a href="mailto:plfa-interest@inf.ed.ac.uk">plfa-interest@inf.ed.ac.uk</a>.</div><div><br></div><div>I've added proj₂ to the imports for Qualifiers. Thanks for pointing it out.</div><div><br></div><div>Go well, -- P</div><div><br></div><div><br></div><div><br></div><div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 17 Apr 2020 at 11:35, Michel Levy <<a href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</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>
<p>I'm always studying plfa. Now I study the chapter Quantifiers. <br>
</p>
<p>In this chapter the first exercise is to prove</p>
<p>∀-distrib-× : {A : Set}{B C : A -> Set} -><br>
((x : A) -> B x × C x) ≃ ((x : A) -> B x) × ((x : A) ->
C x)</p>
<p>But in the import, at the beginning of this chapter, I see<a id="gmail-m_7953612435086325113452"> : open</a> <a id="gmail-m_7953612435086325113457">import</a> <a id="gmail-m_7953612435086325113464" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" target="_blank">Data.Product</a> <a id="gmail-m_7953612435086325113477">using</a> <a id="gmail-m_7953612435086325113483">(</a><a id="gmail-m_7953612435086325113484" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" target="_blank">_×_</a><a id="gmail-m_7953612435086325113487">;</a> <a id="gmail-m_7953612435086325113489" href="https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#225" target="_blank">proj₁</a><a id="gmail-m_7953612435086325113494">)</a> <a id="gmail-m_7953612435086325113496">renaming</a> <a id="gmail-m_7953612435086325113505">(</a><a id="gmail-m_7953612435086325113506" href="https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#209" target="_blank">_,_</a>
<a id="gmail-m_7953612435086325113510">to</a> <a id="gmail-m_7953612435086325113513" href="https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#209" target="_blank">⟨_,_⟩</a><a id="gmail-m_7953612435086325113518">)</a><br>
</p>
<p>Why proj<u></u><u></u><u></u><u></u><u></u><u></u><u></u><u></u><u></u><u></u><u></u><u></u><u></u>2<u></u><u></u><u></u><u></u>proj_2<u></u><u></u><u></u>
necessary to solve this exercise is not in the using list ?</p>
<p>Where should I write these remarks, in this mail list or in the
mail list <a href="mailto:plfa-interest@inf.ed.ac.uk" target="_blank">plfa-interest@inf.ed.ac.uk</a>.<br>
</p>
<div>-- <br>
courriel : <a href="mailto:michel.levy.imag@free.fr" target="_blank">michel.levy.imag@free.fr</a> <br>
mobile : 06 59 13 42 53<br>
web : <a href="http://michel.levy.imag.free.fr" target="_blank">michel.levy.imag.free.fr</a>
</div>
</div>
_______________________________________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>