From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Wed, 14 Sep 2016 20:56:15 +0000 (-0400)
Subject: direct definition of retract
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=fd996327f0da9cf06f455b6c7c3d5be50a7ff635;p=cubicaltt.git

direct definition of retract
---

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