From 5a4c8fbddc0ed33df5ae2898e96daf82174c43eb Mon Sep 17 00:00:00 2001 From: coquand Date: Tue, 29 Dec 2015 16:03:42 +0100 Subject: [PATCH] updated sigma, not use of J --- examples/sigma.ctt | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/examples/sigma.ctt b/examples/sigma.ctt index 40ab04a..3633e7c 100644 --- a/examples/sigma.ctt +++ b/examples/sigma.ctt @@ -1,7 +1,6 @@ module sigma where --- import deppath -import equiv +import prelude -- application of this fact @@ -27,14 +26,10 @@ propSig (A:U) (B:A-> U) (pA:prop A) (pB : (x:A) -> prop (B x)) (t u : sig A B) : = lem A B pB t u (pA t.1 u.1) lemTransp (A:U) (a:A) : Id A a (transport (<_>A) a) = fill (<_>A) a [] --- genComp (<_>A) a [(i=0) -> <_>a] -funDepTr (A:U) (P:A->U) (a0 :A) : (a1:A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) -> +funDepTr (A:U) (P:A->U) (a0 a1 :A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) : Id U (IdP ( P (p@i)) u0 u1) (Id (P a1) (transport ( P (p@i)) u0) u1) = - J A a0 (\ (a1:A) (p:Id A a0 a1) -> (u0:P a0) (u1:P a1) -> - Id U (IdP ( P (p@i)) u0 u1) (Id (P a1) (transport ( P (p@i)) u0) u1)) rem - where rem (u0 u1:P a0) : Id U (Id (P a0) u0 u1) (Id (P a0) (transport (<_>P a0) u0) u1) = - Id (P a0) (lemTransp (P a0) u0@i) u1 + IdP (P (p@j\/i)) (comp (P (p@j/\i)) u0 [(j=0)-><_>u0]) u1 funDepTr (A0:U) : (A1:U) (P:Id U A0 A1) (u0:A0) (u1:A1) -> Id U (IdP P u0 u1) (Id A1 (transport P u0) u1) = -- 2.34.1