merge

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`.

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/
 ---
 
 ```

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 <!-- [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) --> 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 <!-- [Assignment 5]({{ site.baseurl }}/courses/tspl/2010/Mock1.pdf) --> cw5 due 4pm Thursday 21 November (Week 10)
   <!-- <br />
   Use file [Exam]({{ site.baseurl }}/TSPL/2018/Exam/). Despite the rubric, do **all three questions**. -->
@@ -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.
+
 
 <!--
 

src/plfa/part1/Lists.lagda.md

@@ -958,11 +958,11 @@ 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
@@ -970,11 +970,24 @@ 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`.
@@ -1031,7 +1044,7 @@ decidable, using `_∷_` rather than `⟨_,_⟩` to combine the evidence for
 the head and tail of the list.
 
 
-#### Exercise `any?` (stretch)
+#### Exercise `Any?` (stretch)
 
 Just as `All` has analogues `all` and `All?` which determine whether a
 predicate holds for every element of a list, so does `Any` have

src/plfa/part1/Relations.lagda.md

@@ -773,7 +773,7 @@ if it consists of a single zero (representing zero).
 
 Show that increment preserves canonical bitstrings:
 
-    Can x
+    Can b
     ------------
     Can (inc b)
 

src/plfa/part2/Inference.lagda.md

@@ -584,7 +584,7 @@ ext∋ : ∀ {Γ B x y}
     -----------------------------
   → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
 ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
-ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
+ext∋ _   ¬∃ ⟨ A , S _ ∋x ⟩  =  ¬∃ ⟨ A , ∋x ⟩
 ```
 Given a type `A` and evidence that `Γ , y ⦂ B ∋ x ⦂ A` holds, we must
 demonstrate a contradiction.  If the judgment holds by `Z`, then we
@@ -604,7 +604,7 @@ lookup (Γ , y ⦂ B) x with x ≟ y
 ... | yes refl                    =  yes ⟨ B , Z ⟩
 ... | no x≢y with lookup Γ x
 ...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
-...             | yes ⟨ A , ⊢x ⟩  =  yes ⟨ A , S x≢y ⊢x ⟩
+...             | yes ⟨ A , ∋x ⟩  =  yes ⟨ A , S x≢y ∋x ⟩
 ```
 Consider the context:
 
@@ -1027,7 +1027,7 @@ Next, we give the code to erase a lookup judgment:
 ```
 ∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp
 ∥ Z ∥∋               =  DB.Z
-∥ S x≢ ⊢x ∥∋         =  DB.S ∥ ⊢x ∥∋
+∥ S x≢ ∋x ∥∋         =  DB.S ∥ ∋x ∥∋
 ```
 It simply drops the evidence that variable names are distinct.
 

src/plfa/part2/Lambda.lagda.md

@@ -1359,7 +1359,7 @@ or explain why there are no such types.
 2. `` ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ` "x" · (` "y" · ` "z") ⦂ C ``
 
 
-#### Exercise `mul-type` (recommended)
+#### Exercise `⊢mul` (recommended)
 
 Using the term `mul` you defined earlier, write out the derivation
 showing that it is well typed.
@@ -1369,7 +1369,7 @@ showing that it is well typed.
 ```
 
 
-#### Exercise `mulᶜ-type` (practice)
+#### Exercise `⊢mulᶜ` (practice)
 
 Using the term `mulᶜ` you defined earlier, write out the derivation
 showing that it is well typed.