<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<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="452" class="Keyword" moz-do-not-send="true"> : open</a> <a
id="457" class="Keyword" moz-do-not-send="true">import</a> <a
id="464"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html"
class="Module" moz-do-not-send="true">Data.Product</a> <a
id="477" class="Keyword" moz-do-not-send="true">using</a> <a
id="483" class="Symbol" moz-do-not-send="true">(</a><a id="484"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162"
class="Function Operator" moz-do-not-send="true">_×_</a><a
id="487" class="Symbol" moz-do-not-send="true">;</a> <a
id="489"
href="https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#225"
class="Field" moz-do-not-send="true">proj₁</a><a id="494"
class="Symbol" moz-do-not-send="true">)</a> <a id="496"
class="Keyword" moz-do-not-send="true">renaming</a> <a id="505"
class="Symbol" moz-do-not-send="true">(</a><a id="506"
href="https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#209"
class="InductiveConstructor Operator" moz-do-not-send="true">_,_</a>
<a id="510" class="Symbol" moz-do-not-send="true">to</a> <a
id="513"
href="https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#209"
class="InductiveConstructor Operator" moz-do-not-send="true">⟨_,_⟩</a><a
id="518" class="Symbol" moz-do-not-send="true">)</a><br>
</p>
<p>Why proj<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi></mi><mi></mi><mi></mi><msub><mi></mi><mn>2</mn></msub></mrow><annotation
encoding="TeX">proj_2</annotation></semantics></math>
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 class="moz-txt-link-abbreviated"
href="mailto:plfa-interest@inf.ed.ac.uk" moz-do-not-send="true">plfa-interest@inf.ed.ac.uk</a>.<br>
</p>
<div class="moz-signature">-- <br>
courriel : <a class="moz-txt-link-abbreviated" href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a> <br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr
</div>
</body>
</html>