direct definition of retract

diff --git a/examples/retract.ctt b/examples/retract.ctt
index e11548f785d483dc7daea518cd43405a502fcf78..72a11f034e75614fa4546814c129671f5119a99f 100644 (file)
--- a/examples/retract.ctt
+++ b/examples/retract.ctt
@@ -2,9 +2,9 @@ module retract where
 \r
 import prelude\r
 \r
-section (A B : U) (f : A -> B) (g : B -> A) :U = (b : B) -> Path B (f (g b)) b\r
+section (A B : U) (f : A -> B) (g : B -> A) : U = (b : B) -> Path B (f (g b)) b\r
 \r
-retract (A B : U) (f : A -> B) (g : B -> A) : U = section B A g f\r
+retract (A B : U) (f : A -> B) (g : B -> A) : U = (a : A) -> Path A (g (f a)) a\r
 \r
 lemRetract (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y:A) :\r
              Path A (g (f x)) (g (f y)) -> Path A x y\r