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.