∀-× (Quantifiers): Is plfa.Isomorphism.extensionality enough?

[collares]

If I try to prove ∀-distrib-× using the same proof for from∘to as I did in →-distrib-× (using plfa.Isomorphism.extensionality), I get the following somewhat confusing error message in Agda 2.5.4.1:

Cannot instantiate the metavariable _32 to solution B x × C x since
it contains the variable x which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
when checking that the inferred type of an application
  _f_33 f ≡ _g_34 f
matches the expected type
  (λ { ⟨ f , g ⟩ → λ { a → ⟨ f a , g a ⟩ } })
  ((λ { f → ⟨ (λ x → proj₁ (f x)) , (λ x → proj₂ (f x)) ⟩ }) f)
  ≡ f

However, if I postulate agda-stdlib's version of extensionality instead of using plfa.Isomorphism.extensionality, which is

postulate
  extensionality : ∀ {a b : Level} {A : Set a} {B : A → Set b}
    {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g

then everything works fine. My question is: Is the extensionality postulate from plfa.Isomorphism enough to do this exercise?

[wadler]

Thanks for your note. Please send the exact code that failed. Minimise the file if you can, so it contains all the relevant code but nothing else. Then I may be able to help.

[collares]

Sorry for not doing this earlier! Since I understand this exercise is in a due assignment for the PUC course, I was trying to avoid "spoilers". Here's the file: https://gist.github.com/collares/5afa808eef7f647190e0dea244e6eb50

[collares]

Sorry, I now have a clue as to where I went wrong: If I use Data.Product.× instead of plfa.Isomorphism.×, then I don't need any sort of extensionality for the proof. If, however, I use × and η-× from plfa.Connectives, then I get the error. I guess the definition of product we did was simplified (wrt levels) for educational purposes?

[h4iku]

I think the same thing also happens in the from∘to part of the ∀-× exercise. It doesn't work with plfa.Isomorphism's extensionality and gives a similar error message, but works with the one posted by @collares.

Gist: https://gist.github.com/h4iku/ddc0ee5b19eca85e8877af93fd632e3c

[Boarders]

I ran into the same issue in the ∀-× exercise. The issue is that the book version of extensionality:

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

does not allow the dependent function type (i.e. B is not dependent on A). This means that when one tries to prove an equality in the type:

(p q : ∀ (t : Tri) -> B t) -> p ≡ q

Then the book's version of extensionality doesn't cut it.

[collares]

I renamed this issue since the problem with ∀-× affects even people using the book imports, whereas my original issue was specific to using plfa.Isomorphism.× instead of Data.Product.×.

[adql]

This exercise can be solved without using ∀-extensionality (as suggested above). I think the hint could be removed.