From 31e38f1eb5e96523ed341591c125981528d3b4fa Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Mon, 20 Apr 2015 23:22:12 +0200 Subject: [PATCH] Fix retract --- examples/retract.ctt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ( g (pB (f x) (f y)) @ i) + : Id A x y = lemRetract A B f g rfg x y ( 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 = -- 2.34.1