diff --git a/Exe1.agda b/Exe1.agda
index 998086a..36dc573 100644
--- a/Exe1.agda
+++ b/Exe1.agda
@@ -147,6 +147,8 @@ VecN n = One / pure n
 ListN : Normal
 ListN = Nat / id
 
+-- These exercises don't appear anywhere, but we did cover them during
+-- the lecture. I added a placemarker in the notes for this.
 
 K : Set -> Normal
 K A = {!!}
diff --git a/Vec.lagda b/Vec.lagda
index cab08d8..cc92c18 100644
--- a/Vec.lagda
+++ b/Vec.lagda
@@ -684,6 +684,9 @@ Note that |<?>| has been defined to work at all levels of the predicative
 hierarchy, so that we can use it to choose between |Set|s, as well as between
 ordinary values. |Sg| thus models both choice and pairing in data structures.
 
+TODO: Insert exercise/comment regarding constant functors and the
+identity being normal.
+
 I don't know about you, but I find I do a lot more arithmetic with types than I
 do with numbers, which is why I have used |*| and |+| for |Set|s. Developing a
 library of normal functors will, however, necessitate arithmetic on sizes as
@@ -767,7 +770,7 @@ nOut : forall {X}(F G : Normal) -> <! F +N G !>N X -> <! F !>N X + <! G !>N X
 nOut F G xs' with nCase F G xs'
 nOut F G .(nInj F G xs) | from xs = xs
 \end{code}
-The |with| notation allows us to compute smoe useful information and add
+The |with| notation allows us to compute some useful information and add
 it to the collection of things available for inspection in pattern matching.
 By matching the result of |nCase F G xs'| as |from xs|, we discover that
 \emph{ipso facto}, |xs'| is |nInj xs|. It is in the nature of dependent