diff --git a/courses/tspl/2019/Assignment3.lagda.md b/courses/tspl/2019/Assignment3.lagda.md index c1782e0b..5e00b72d 100644 --- a/courses/tspl/2019/Assignment3.lagda.md +++ b/courses/tspl/2019/Assignment3.lagda.md @@ -220,6 +220,7 @@ replacement for `_×_`. As a consequence, demonstrate an equivalence relating -- Your code goes here ``` + #### Exercise `All-++-≃` (stretch) Show that the equivalence `All-++-⇔` can be extended to an isomorphism. @@ -228,11 +229,12 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism. -- Your code goes here ``` -#### Exercise `¬Any≃All¬` (recommended) + +#### Exercise `¬Any⇔All¬` (recommended) Show that `Any` and `All` satisfy a version of De Morgan's Law: - (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs + (¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs (Can you see why it is important that here `_∘_` is generalised to arbitrary levels, as described in the section on @@ -240,11 +242,26 @@ to arbitrary levels, as described in the section on Do we also have the following? - (¬_ ∘ All P) xs ≃ Any (¬_ ∘ P) xs + (¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs If so, prove; if not, explain why. +``` +-- Your code goes here +``` + + +#### Exercise `¬Any≃All¬` (stretch) + +Show that the equivalence `¬Any⇔All¬` can be extended to an isomorphism. +You will need to use extensionality. + +``` +-- Your code goes here +``` + + #### Exercise `All-∀` (practice) Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`. diff --git a/courses/tspl/2019/Assignment4.lagda.md b/courses/tspl/2019/Assignment4.lagda.md index e1ee7734..81a5b661 100644 --- a/courses/tspl/2019/Assignment4.lagda.md +++ b/courses/tspl/2019/Assignment4.lagda.md @@ -1,7 +1,7 @@ --- title : "Assignment4: TSPL Assignment 4" layout : page -permalink : /TSPL/2018/Assignment4/ +permalink : /TSPL/2019/Assignment4/ --- ``` diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index 10167f08..1292bd74 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -122,7 +122,7 @@ For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.ba * [Assignment 1]({{ site.baseurl }}/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3) * [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5) * [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7) -* Assignment 4 cw4 due 4pm Thursday 14 November (Week 9) +* [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) cw4 due 4pm Thursday 14 November (Week 9) * Assignment 5 cw5 due 4pm Thursday 21 November (Week 10) @@ -144,6 +144,13 @@ but talk to me if you want to formalise something else. * Optional project cw6 due 4pm Thursday 28 November (Week 11) +## Midterm course feedback + +You may offer feedback on the course at +[https://www.surveymonkey.co.uk/r/YX7ZFYC](https://www.surveymonkey.co.uk/r/YX7ZFYC). + +Please do so by 4pm Thursday 31 October. +