[Agda] plfa, using proj2, missing in Quantifiers

[Philip Wadler]

Michel,

Questions like your are welcome on plfa-interest at inf.ed.ac.uk.

I've added proj₂ to the imports for Qualifiers. Thanks for pointing it out.

Go well, -- P




.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Fri, 17 Apr 2020 at 11:35, Michel Levy <michel.levy.imag at free.fr> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200417/9a8ef0d1/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200417/9a8ef0d1/attachment.ksh>