From fd996327f0da9cf06f455b6c7c3d5be50a7ff635 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Wed, 14 Sep 2016 16:56:15 -0400 Subject: [PATCH] direct definition of retract --- examples/retract.ctt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/retract.ctt b/examples/retract.ctt index e11548f..72a11f0 100644 --- a/examples/retract.ctt +++ b/examples/retract.ctt @@ -2,9 +2,9 @@ module retract where import prelude -section (A B : U) (f : A -> B) (g : B -> A) :U = (b : B) -> Path B (f (g b)) b +section (A B : U) (f : A -> B) (g : B -> A) : U = (b : B) -> Path B (f (g b)) b -retract (A B : U) (f : A -> B) (g : B -> A) : U = section B A g f +retract (A B : U) (f : A -> B) (g : B -> A) : U = (a : A) -> Path A (g (f a)) a lemRetract (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y:A) : Path A (g (f x)) (g (f y)) -> Path A x y -- 2.34.1