From: Anders Mörtberg <mortberg@chalmers.se>
Date: Mon, 20 Apr 2015 21:22:12 +0000 (+0200)
Subject: Fix retract
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=31e38f1eb5e96523ed341591c125981528d3b4fa;p=cubicaltt.git

Fix retract
---

diff --git a/examples/retract.ctt b/examples/retract.ctt
index 34d3559..9c9c89f 100644
--- 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)
 
 retractProp (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (pB :prop B) (x y:A) 
-  : Id A x y = lemRetract A B f g rfg x y (<i> g (pB (f x) (f y)) @ i)
+  : Id A x y = lemRetract A B f g rfg x y (<i> g (pB (f x) (f y) @ i))
 
 retractInv (A B : U)  (f : A -> B) (g : B -> A) (rfg : retract A B f g)
            (x y : A) (q: Id B (f x) (f y)) : Id A x y =