update TSPL for 2023-09-22 (#914)

* update TSPL for 2023-09-22

* [pre-commit.ci] auto fixes from pre-commit.com hooks

for more information, see https://pre-commit.ci

---------

Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com>

courses/TSPL/2023/Assignment1.lagda.md

@@ -19,7 +19,8 @@ You don't need to do all of these, but should attempt at least a few.
 
 Exercises labelled "(practice)" are included for those who want extra practice.
 
-Submit your homework using the "submit" command.
+Submit your homework using Gradescope. Go to the course page under Learn.
+Select `Assessment`, then select `Assignment Submission`.
 Please ensure your files execute correctly under Agda!
 
 
@@ -410,7 +411,7 @@ As with inequality, some additional definitions may be required.
   -- Your code goes here
 ```
 
-#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
+#### Exercise `≤→<, <→≤` (recommended) {#leq-iff-less}
 
 Show that `suc m ≤ n` implies `m < n`, and conversely.
 

courses/TSPL/2023/tspl.md

@@ -56,43 +56,43 @@ Each lecture is immediately followed by a tutorial.
  </tr>
  <tr>
   <td>2</td>
-  <td>**25 Sep**
-  <td>**28 Sep**
+  <td>**25 Sep** </td>
+  <td>**28 Sep** </td>
  </tr>
  <tr>
   <td>3</td>
-  <td> **2 Oct**
-  <td> **4 Oct**
+  <td> **2 Oct** [Equality](/Equality/) (no class, read on your own)</td>
+  <td> **4 Oct** [Isomorphism](/Isomorphism/) (no class, read on your own)</td>
  </tr>
  <tr>
   <td>4</td>
-  <td>**9 Oct** [Equality](/Equality/) &amp; [Isomorphism](/Isomorphism/)</td>
-  <td>**11 Oct** [Connectives](/Connectives/)
+  <td>**9 Oct** [Connectives](/Connectives/)</td>
+  <td>**11 Oct** [Negation](/Negation/)</td>
  </tr>
  <tr>
   <td>5</td>
-  <td>**16 Oct** [Negation](/Negation/)</td>
-  <td>**18 Oct** [Quantifiers](/Quantifiers/)</td>
+  <td>**16 Oct** [Quantifiers](/Quantifiers/)</td>
+  <td>**18 Oct** [Decidable](/Decidable/)</td>
  </tr>
  <tr>
   <td>6</td>
-  <td>**23 Oct** [Decidable](/Decidable/) &amp; [Lists](/Lists/)</td>
-  <td>**25 Oct** [Lambda](/Lambda/)</td>
+  <td>**23 Oct** [Lambda](/Lambda/)</td>
+  <td>**25 Oct** [Properties](/Properties/)</td>
  </tr>
  <tr>
   <td>7</td>
-  <td>**30 Oct** [Properties](/Properties/)</td>
-  <td> **1 Nov** [DeBruijn](/DeBruijn/)</td>
+  <td>**30 Oct** [DeBruijn](/DeBruijn/)</td>
+  <td> **1 Nov** [More](/More/)</td>
  </tr>
  <tr>
   <td>8</td>
-  <td> **6 Nov** [More](/More/)</td>
-  <td>**8 Nov** [Inference](/Inference/)</td>
+  <td> **6 Nov** [Inference](/Inference/)</td>
+  <td>**8 Nov** [Untyped](/Untyped/)</td>
  </tr>
  <tr>
   <td>9</td>
-  <td>**13 Nov** [Untyped](/Untyped/)</td>
-  <td>**15 Nov** [Eval](/TSPL/2022/Eval/)</td>
+  <td>**13 Nov** [Eval](/TSPL/2022/Eval/)</td>
+  <td>**15 Nov** </td>
  </tr>
  <tr>
   <td>10</td>