Type suggested in exercise Bin-isomorphism does not compile.

[nrnrnr]

In the Quantifiers chapter, the proj₁ imported from Data.Product is not compatible with the Σ defined in the chapter. But in exercise Bin-isomorphism, it is suggested to prove a lemma of this type:

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

Because of the incompatibility in proj₁, the type will not compile.

I was not able to figure out this issue until I had completed all of Part 1.

[wadler]

Thanks, Norman.

Why weren't you using both proj₁ and ∃ from Chapter Quantifiers? Then it should work.

If you submit a pull request with text or code changes that would have saved you confusion, I'll be happy to consider it.

(In general, the fact that chapters define their own code incompatible with the library code is a persistent problem throughout PLFA. In Lean, they use a style where each code snippet has its own separate imports. That might be one way around the problem, except that Agda has no support for that style.)

[nrnrnr]

I used both the proj₁ and the ∃ (Σ) that were in scope. That's the issue. The ∃ and Σ are defined in the chapter, but proj₁ is imported from Data.Product. The two aren't compatible.

A sample error message:

/home/nr/cs/plfa/part1/Quantifiers.lagda.md:541,46-47
(Σ Bin (λ b → Can b)) !=< (Data.Product.Σ _A_260 _B_261)
when checking that the expression c has type
Data.Product.Σ _A_260 _B_261