part1/Quantifiers: exercise requires proj₁, which can't be imported nor defined due to conflicts

[lorenzo-lipparini]

Exercise Bin-isomorphism asks the reader to give evidence for:

proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′

But, when the user attempts the exercise he is faced with an error:

postulate
  Bin : Set
  Can : Bin → Set

proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
proj₁≡→Can≡ = {!!}

(Σ Bin (λ b → Can b)) !=< (Data.Product.Σ _A_156 _B_157)
when checking that the expression cb has type
Data.Product.Σ _A_156 _B_157

This is due to the fact that the current file imports proj₁ from Data.Product, meaning that proj₁ will work on the Σ type from the stdlib, but not on the Σ type defined in this chapter.

I'm not sure how it would be best to handle this problem, but here are a few observations:

1. Although the module imports proj₁ and proj₂, it doesn't actually use them, hence we could remove those imports and ask the reader to define a suitable proj₁ for the Σ in this chapter; but, the problem would arise again if the reader himself imports proj₁ to solve previous exercises.
2. The exercise could be reframed in terms of Σ′ which has been defined as a record, with a proj₁′ function available already; but this way we'd lose the nice syntax which has been defined for Σ.
3. We could explicitly mention the conflict, and ask the reader to define a proj₁′ function for the Σ type in this chapter (this should not create conficts with Σ′, as its projection is namespaced as Σ′.proj₁′).

[wadler]

Thanks for pointing this out. I suggest you write out a full solution to the problem using one of the proposed techniques, and then submit a pull request to modify the problem accordingly. Option 1 may be best, combined with option 3 to warn the user of the problem. You should also file your solution in our solutions repository, https://github.com/wadler/plfa-answers; send a request for access and it will be granted.

[lorenzo-lipparini]

Thanks @wadler, I'll be happy to work on this in the next days.

Where should I send the request to access the repository with the solutions? Is there a form to fill in or something similar? It seems the link above will return a 404 until I get access rights.

[wadler]

Waiting on CI to work before accepting a change to Agda code. I hope CI will be fixed soon!

[wenkokke]

It’s already working, actually.