Exercise ⊎-dual-× (part1.Negation): add a note about imports

[adql]

This exercise notes that its result "is an easy consequence of something we've proved previously."

I'm fairly certain my solution got it right. However, it involves imports that might lead to confusions: Negation.lagda.md imports some type definitions used in this exercise from the standard library, while the module where something was "proved previously" defines these types by itself. This leads to type mismatch. A note suggesting to import these types with renaming to ′-ed versions (in addition to the necessary proof itself) would be helpful.

(Please excuse my somewhat awkward formulation, I'm trying to avoid exposing the solution.)

[wadler]

Thank you for the suggestion!

You are correct about the type mismatch and it is annoying. But I'm not sure if your hint would help. The problem is formulated without the primed versions:
¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
So how would importing primed versions help?

[wenkokke]

I believe that's exactly the issue that @adql it's raising. Perhaps the exercise should be stated over primed versions, explicitly imported as part of the exercise, so that the student can actually prove the property using the previous result?

[adql]

Yes, the point is that the user expects to solve the exercise with the provided type signature, but this never works with the import from the other module. By "primed versions" I mean the types defined locally in the same module as the needed proof.

Explicitly importing primed versions would be helpful, especially if the student is not expected to do renaming imports by themselves at this stage. But of course it would also hint at the source of the required proof.