Quantifiers, Bin-Isomorphism exercise: issue with type of proj₁≡→Can≡

[matthew-healy]

I've just completed the Bin-Isomorphism exercise at the end of the Quantifiers chapter.

As part of the exercise, it is suggested that the reader proves the following lemma:

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

However, having typed up the definitions from the chapter directly, and then this lemma, I get the following on attempting to load the file:

(∑ Bin (λ b → Can b)) !=< (Data.Product.Σ _A_284 _B_285) of type
Set
when checking that the expression cb has type
Data.Product.Σ _A_284 _B_285

The error itself makes sense - we've imported proj₁ from the standard library but we've defined ∃ by hand, and there's no reason they should play nicely together. However, up until this point in the book everything we've defined has either worked fine with the standard library or it's been called out that this could be a problem.

Is it perhaps worth calling this out as part of the exercise and suggesting either that the reader re-implements proj₁ to work with our custom ∃, or that they import ∃ from the standard library? I'm happy to submit something like this, but wanted to check it was desirable first.

[wadler]

Thanks, Matthew! Excellent point.

I think the right way to fix this is to introduce proj_1 and proj_2 directly for existentials when they are introduced. As I recall, Wen wanted to reengineer product, unit, and existential to be defined by record first and datatype second (it's currently the other way around), which would fix this automatically. Wen, where are you with this project?

(PS. In reviewing the text, I note that product and unit are currently introduced by the phrase "we define a suitable record type" when it should be "we define a suitable inductive type".)

[wadler]

Thanks, Matthew! Excellent point.

I think the right way to fix this is to introduce proj_1 and proj_2 directly for existentials when they are introduced. As I recall, Wen wanted to reengineer product, unit, and existential to be defined by record first and datatype second (it's currently the other way around), which would fix this automatically. Wen, where are you with this project?

(PS. In reviewing the text, I note that product and unit are currently introduced by the phrase "we define a suitable record type" when it should be "we define a suitable inductive type".)

[wenkokke]

@wadler Was this fixed?