From 4947b427f9c96b599f8c2f281d13379ed755e6ea Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 4 Jun 2015 21:43:20 +0200 Subject: [PATCH] define trans in terms of gencomp --- examples/prelude.ctt | 5 +++++ 1 file changed, 5 insertions(+) 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 = \(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 -- 2.34.1