Type of suggested lemma in Bin-isomorphism compiles

[negatratoron]

Fixes #1003

The type signature compiles by qualifying the function "proj_1". Also added a sentence calling this out.

[wadler]

Thank you!

I try to avoid using qualifiers. I think a better fix would be to remove the import of Data.Product at the beginning of the chapter. Would you be willing to make a pull request to that effect?

[negatratoron]

Ahh, I think the problem is the Sigma record was not opened. I was a little surprised Agda didn't figure out that proj_1 referred to the Sigma field, turns out that's because it wasn't in scope.

[wadler]

Well spotted. I'm always forgetting to open records. Thanks for that save!

I think it's important also to remove the import of Data.Product, else there will be a clash of names. Can you do that as well?

And with the import removed, the definition of \times' can lose the prime (and the sentence drawing attention to the prime). Could you please make this fix as well?

Thank you for your help!

[negatratoron]

I think it's important also to remove the import of Data.Product, else there will be a clash of names. Can you do that as well?

That definition is used in the Universals exercises, so I don't think it can just be deleted. The definition has to exist for those exercises to compile.

You're welcome :)

[negatratoron]

Re-requesting a review. I don't think the Data.Product import could be removed (other than by re-defining products or importing the earlier Connectives chapter) without significantly affecting the Universals exercises (somehow removing product from them, or moving them below the product definition in the Existentials section).

[wadler]

Elsewhere in the chapter, \times is defined. (Once you remove the prime, as I requested previously.) And it is defined in terms of \Sigma, so has proj_1 and proj_2 defined. So the exercises will be fine, they just use the product defined in the chapter, which is defined in exactly the same way as in Data.Product.

More generally, there is a tension between using the operations as defined in the chapters and using the operations from the Standard Library. In Lean, documentation is sometimes written with a separate, hidden set of imports for each code block. That has the advantage of being able to define product in one code block and then use the one imported from the standard library in the next code block. But it has the disadvantage that if you read the book without opening each block you don't know what imports are in scope.

[negatratoron]

Maybe I don't understand what you're saying, but if I make this change: negatratoron@472f8bb

I get an error "Not in scope: \times" from the exercise on line 94.

From the Agda docs:

Names must be declared before they are used

Separating the signature from the definition is possible, but these exercises depend on the definition of \times, so it's not enough to just declare "\times : Set \to Set \to Set", it has to have its full definition present.

The key thing is, \times is used in exercises before products are defined in terms of Sigma.