[Agda] plfa, using proj2, missing in Quantifiers

[Michel Levy]

I'm always studying plfa. Now I study the chapter Quantifiers.

In this chapter the first exercise is to prove

∀-distrib-× : {A : Set}{B C : A -> Set} ->
  ((x : A) -> B x × C x) ≃ ((x : A) -> B x) × ((x : A) -> C x)

But in the import, at the beginning of this chapter, I see: open import
Data.Product <https://agda.github.io/agda-stdlib/v1.1/Data.Product.html>
using (_×_
<https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162>; proj₁
<https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#225>)
renaming (_,_
<https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#209> to
⟨_,_⟩ <https://plfa.github.io/Quantifiers/Agda.Builtin.Sigma.html#209>)

Why proj2proj_2 necessary to solve this exercise is not in the using list ?

Where should I write these remarks, in this mail list  or in the mail
list plfa-interest at inf.ed.ac.uk.

-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200417/609e7b10/attachment.html>