define trans in terms of gencomp

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 925118259476f9b066cb53b57cbf4282ba0fd556..a185e9d9f160dc7279ad62ace1ae48d499c43134 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -15,6 +15,11 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
        (p : (x : A) -> Id (B x) (f x) (g x)) :
        Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i
 
+trans (A B : U) (p : Id U A B) (a : A) : B = genComp p a []
+
+-- subst can be defined using trans:
+substTrans (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
+  trans (P a) (P b) (mapOnPath A U P a b p) e
 
 subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
   transport (mapOnPath A U P a b p) e