All-∀ exercise

[Boarders]

This exercise asks us to prove an isomorphism:

 All P xs ≃ (∀ {x} -> x ∈ xs -> P x)

I believe this is only possible with the version of dependent extensionality discussed here.

[collares]

Besides this, one other thing confused me in this exercise: When you have an implicit function such as f : (∀ {x} → x ∈ xs → P x) in a type signature, Agda will try to find a variable to solve the implicit argument whenever you use f later on, so naïve attempts to solve this exercise will result in lots of yellow. The trick is to do (λ {x} → f {x}) instead of just f if you don't want the default behaviour. It would be nice to mention this trick somewhere, since I don't recall it being needed in previous exercises.

[Boarders]

@collares : Good point! I had to resort to writing it out explicitly as I was unable to deal with what was implicitly brought into scope.

[collares]

If you want to solve it with implicit arguments, this is the version of extensionality I used, courtesy of a kind soul in the Agda IRC channel whose name I unfortunately can't remember:

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

Edit: Oh wait, I see that tomjack helped you with your other issue. He's the one who helped me as well!

[wadler]

Thank you. All good points! It's fairly subtle, so I'm not sure whether the best thing is to explain these points or delete the exercise. If someone suggests appropriate text, I'm likely to include it.

[Boarders]

I found these exercises quite challenging but also illuminating and so think it would be a shame to see them go! Personally on such exercises, which includes (I believe):

Quantifiers.∀-×
List.All-∀
List.Any-∃

I would add something like this the first time around:

Since we are trying to prove an isomorphism between dependent function types 
we will need a new principle of extensionality for such things:

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

And then at the later exercises you can say something of the form:

As this is an isomorphism between dependent function types we will again need a
 `dependent-extensionality` principle (as in exercise [blah]). Feel free to write your 
own such principle or use the one provided there.

The dependent-extensionality principle I have written here is enough to solve each of the exercises but I'm unsure if it leads people down the garden path too much.

[wadler]

The section on extensionality in Chapter Isomorphism now states: "More generally, we may wish to postulate extensionality for dependent functions" and introduces a suitable postulate named ∀-extensionality. So all that is necessary is to add a line to the exercises mentioned citing ∀-extensionality. Would one of you be willing to add a pull request along these lines? I would do it, but I think it is important to check that ∀-extensionality is actually required, and I don't have time to do that. Thank you for your help.