Connectives: fixes the text of exercises to match names of proofs
Closes #187.
This commit is contained in:
parent
a08d25d6a9
commit
33f46517cf
1 changed files with 2 additions and 2 deletions
|
@ -491,7 +491,7 @@ is the identity of sums _up to isomorphism_.
|
|||
|
||||
#### Exercise `⊥-identityˡ` (recommended)
|
||||
|
||||
Show zero is the left identity of addition.
|
||||
Show empty is the left identity of sums up to isomorphism.
|
||||
|
||||
\begin{code}
|
||||
-- Your code goes here
|
||||
|
@ -499,7 +499,7 @@ Show zero is the left identity of addition.
|
|||
|
||||
#### Exercise `⊥-identityʳ`
|
||||
|
||||
Show zero is the right identity of addition.
|
||||
Show empty is the right identity of sums up to isomorphism.
|
||||
|
||||
\begin{code}
|
||||
-- Your code goes here
|
||||
|
|
Loading…
Reference in a new issue