Fix retract

diff --git a/examples/retract.ctt b/examples/retract.ctt
index 34d3559c760933197035f5f85b4e3775d5478cf3..9c9c89f77a35f9f6358c53b98e3644464db2779f 100644 (file)
--- a/examples/retract.ctt
+++ b/examples/retract.ctt
@@ -11,7 +11,7 @@ lemRetract (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y:A) :
   = compUp A (g (f x)) x (g (f y)) y (rfg x) (rfg y)\r
 \r
 retractProp (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (pB :prop B) (x y:A) \r
-  : Id A x y = lemRetract A B f g rfg x y (<i> g (pB (f x) (f y)) @ i)\r
+  : Id A x y = lemRetract A B f g rfg x y (<i> g (pB (f x) (f y) @ i))\r
 \r
 retractInv (A B : U)  (f : A -> B) (g : B -> A) (rfg : retract A B f g)\r
            (x y : A) (q: Id B (f x) (f y)) : Id A x y = \r