diff --git a/tex/chTT.tex b/tex/chTT.tex
index f19f51e..d26e94b 100644
--- a/tex/chTT.tex
+++ b/tex/chTT.tex
@@ -384,7 +384,7 @@ \section{Terms, types, sorts}\label{sec:terms}
 Check Set : Type.
 \end{coq-left}
 \begin{coqout-right}
-Set : Type@{U4} (* Set < U3 *)
+Set : Type@{U4} (* Set < U4 *)
 \end{coqout-right}
 \coqrun{name=r2}{ssr,check-set}