Remove remaining TODO

Author: ionathanch

main.pdf

@@ -112,7 +112,7 @@ \section{Introduction}
 \begin{quote}
     Although the notion of a CwR covers a wide range of type theories including Martin-L\"of type theory,
     univalent type theory, and cubical type theory, it cannot cover some important type theories.
-    Characteristics of type theories considered in [\citet{actt}] are that contexts are single-layered
+    Characteristics of type theories considered [by \citet{actt}] are that contexts are single-layered
     and that assumptions in a context can be used at any time, any number of times.
     Type theories with “dual-contexts” are not of this sort.
     Substructural type theories such as linear logic are out of scope since assumptions can be used a limited number of times.
@@ -140,7 +140,7 @@ \section{Introduction}
     this should follow from initiality.
 \end{enumerate}
 
-The semantic model can be defined in a variety of suitable mathematical theories: it could be a set-theoretic model, a type-theoretic model, a realizability model, and so on. \todo{Be more specific and cite.}
+The semantic model can be defined in a variety of suitable mathematical theories: it could be a set-theoretic model, a type-theoretic model, a presheaf model, a realizability model, and so on.
 
 This note is aimed towards those familiar with the usual formulations of and concepts in type theory.
 Even so, some minimal category-theoretic knowledge is needed to begin promptly.