Fix use of headers

.markdownlint.yaml

@@ -1,11 +1,11 @@
 default: true
-MD001: false
 MD004: false
 MD007: false
 MD012: false
 MD013: false
 MD022: false
 MD024: false
+MD025: false
 MD030: false
 MD032: false
 MD033: false

courses/TSPL/2019/Assignment1.lagda.md

@@ -7,9 +7,9 @@ permalink : /TSPL/2019/Assignment1/
 module Assignment1 where
 ```
 
-## YOUR NAME AND EMAIL GOES HERE
+# YOUR NAME AND EMAIL GOES HERE
 
-## Introduction
+# Introduction
 
 You must do _all_ the exercises labelled "(recommended)".
 
@@ -28,7 +28,7 @@ Please ensure your files execute correctly under Agda!
 
 
 
-## Good Scholarly Practice.
+# Good Scholarly Practice.
 
 Please remember the University requirement as
 regards all assessed work. Details about this can be found at:
@@ -43,7 +43,7 @@ yourself, or your group in the case of group practicals).
 
 
 
-## Imports
+# Imports
 
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
@@ -55,24 +55,24 @@ open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
 open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
 ```
 
-## Naturals
+# Naturals
 
-#### Exercise `seven` (practice) {#seven}
+### Exercise `seven` (practice) {#seven}
 
 Write out `7` in longhand.
 
 
-#### Exercise `+-example` (practice) {#plus-example}
+### Exercise `+-example` (practice) {#plus-example}
 
 Compute `3 + 4`, writing out your reasoning as a chain of equations.
 
 
-#### Exercise `*-example` (practice) {#times-example}
+### Exercise `*-example` (practice) {#times-example}
 
 Compute `3 * 4`, writing out your reasoning as a chain of equations.
 
 
-#### Exercise `_^_` (recommended) {#power}
+### Exercise `_^_` (recommended) {#power}
 
 Define exponentiation, which is given by the following equations.
 
@@ -82,12 +82,12 @@ Define exponentiation, which is given by the following equations.
 Check that `3 ^ 4` is `81`.
 
 
-#### Exercise `∸-examples` (recommended) {#monus-examples}
+### Exercise `∸-examples` (recommended) {#monus-examples}
 
 Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
 
 
-#### Exercise `Bin` (stretch) {#Bin}
+### Exercise `Bin` (stretch) {#Bin}
 
 A more efficient representation of natural numbers uses a binary
 rather than a unary system.  We represent a number as a bitstring.
@@ -134,9 +134,9 @@ For the former, choose the bitstring to have no leading zeros if it
 represents a positive natural, and represent zero by `x0 nil`.
 Confirm that these both give the correct answer for zero through four.
 
-## Induction
+# Induction
 
-#### Exercise `operators` (practice) {#operators}
+### Exercise `operators` (practice) {#operators}
 
 Give another example of a pair of operators that have an identity
 and are associative, commutative, and distribute over one another.
@@ -145,14 +145,14 @@ Give an example of an operator that has an identity and is
 associative but is not commutative.
 
 
-#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
+### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
 
 Write out what is known about associativity of addition on each of the first four
 days using a finite story of creation, as
 [earlier][plfa.Naturals#finite-creation]
 
 
-#### Exercise `+-swap` (recommended) {#plus-swap}
+### Exercise `+-swap` (recommended) {#plus-swap}
 
 Show
 
@@ -166,23 +166,23 @@ the following function from the standard library:
     sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
 
 
-#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
+### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
 
 Show multiplication distributes over addition, that is,
 
     (m + n) * p ≡ m * p + n * p
 
 for all naturals `m`, `n`, and `p`.
 
-#### Exercise `*-assoc` (recommended) {#times-assoc}
+### Exercise `*-assoc` (recommended) {#times-assoc}
 
 Show multiplication is associative, that is,
 
     (m * n) * p ≡ m * (n * p)
 
 for all naturals `m`, `n`, and `p`.
 
-#### Exercise `*-comm` (practice) {#times-comm}
+### Exercise `*-comm` (practice) {#times-comm}
 
 Show multiplication is commutative, that is,
 
@@ -191,23 +191,23 @@ Show multiplication is commutative, that is,
 for all naturals `m` and `n`.  As with commutativity of addition,
 you will need to formulate and prove suitable lemmas.
 
-#### Exercise `0∸n≡0` (practice) {#zero-monus}
+### Exercise `0∸n≡0` (practice) {#zero-monus}
 
 Show
 
     zero ∸ n ≡ zero
 
 for all naturals `n`. Did your proof require induction?
 
-#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
+### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
 
 Show that monus associates with addition, that is,
 
     m ∸ n ∸ p ≡ m ∸ (n + p)
 
 for all naturals `m`, `n`, and `p`.
 
-#### Exercise `Bin-laws` (stretch) {#Bin-laws}
+### Exercise `Bin-laws` (stretch) {#Bin-laws}
 
 Recall that
 Exercise [Bin][plfa.Naturals#Bin]
@@ -228,32 +228,32 @@ over bitstrings.
 For each law: if it holds, prove; if not, give a counterexample.
 
 
-## Relations
+# Relations
 
 
-#### Exercise `orderings` (practice) {#orderings}
+### Exercise `orderings` (practice) {#orderings}
 
 Give an example of a preorder that is not a partial order.
 
 Give an example of a partial order that is not a preorder.
 
 
-#### Exercise `≤-antisym-cases` (practice) {#leq-antisym-cases}
+### Exercise `≤-antisym-cases` (practice) {#leq-antisym-cases}
 
 The above proof omits cases where one argument is `z≤n` and one
 argument is `s≤s`.  Why is it ok to omit them?
 
 
-#### Exercise `*-mono-≤` (stretch)
+### Exercise `*-mono-≤` (stretch)
 
 Show that multiplication is monotonic with regard to inequality.
 
 
-#### Exercise `<-trans` (recommended) {#less-trans}
+### Exercise `<-trans` (recommended) {#less-trans}
 
 Show that strict inequality is transitive.
 
-#### Exercise `trichotomy` (practice) {#trichotomy}
+### Exercise `trichotomy` (practice) {#trichotomy}
 
 Show that strict inequality satisfies a weak version of trichotomy, in
 the sense that for any `m` and `n` that one of the following holds:
@@ -266,26 +266,26 @@ similar to that used for totality.
 (We will show that the three cases are exclusive after we introduce
 [negation][plfa.Negation].)
 
-#### Exercise `+-mono-<` {#plus-mono-less}
+### Exercise `+-mono-<` {#plus-mono-less}
 
 Show that addition is monotonic with respect to strict inequality.
 As with inequality, some additional definitions may be required.
 
-#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
+### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
 
 Show that `suc m ≤ n` implies `m < n`, and conversely.
 
-#### Exercise `<-trans-revisited` (practice) {#less-trans-revisited}
+### Exercise `<-trans-revisited` (practice) {#less-trans-revisited}
 
 Give an alternative proof that strict inequality is transitive,
 using the relating between strict inequality and inequality and
 the fact that inequality is transitive.
 
-#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
+### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
 
 Show that the sum of two odd numbers is even.
 
-#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
+### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
 
 Recall that
 Exercise [Bin][plfa.Naturals#Bin]