<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>