From e52df5dd112fd395868931ce574d2915422021f9 Mon Sep 17 00:00:00 2001
From: Mysaa Java <mysaa@hadoly.fr>
Date: Wed, 1 Apr 2026 17:57:12 +0200
Subject: [PATCH] Fixed typo on page 72

---
 tex/chTT.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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}