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

[negatratoron]

I just ran into this too. Thanks for the explanation @nrnrnr . It looks like the type compiles if I use Σ.proj₁:

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