From: Anders Mörtberg <mortberg@chalmers.se>
Date: Thu, 4 Jun 2015 19:43:20 +0000 (+0200)
Subject: define trans in terms of gencomp
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4947b427f9c96b599f8c2f281d13379ed755e6ea;p=cubicaltt.git

define trans in terms of gencomp
---

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 9251182..a185e9d 100644
--- 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