From: coquand <coquand@chalmers.se>
Date: Tue, 29 Dec 2015 15:03:42 +0000 (+0100)
Subject: updated sigma, not use of J
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=5a4c8fbddc0ed33df5ae2898e96daf82174c43eb;p=cubicaltt.git

updated sigma, not use of J
---

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 []
---  <i>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 (<i> P (p@i)) u0 u1) (Id (P a1) (transport (<i> P (p@i)) u0) u1) =
- J A a0 (\ (a1:A) (p:Id A a0 a1) -> (u0:P a0) (u1:P a1) ->
-             Id U (IdP (<i> P (p@i)) u0 u1) (Id (P a1) (transport (<i> 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) =
-         <i>Id (P a0) (lemTransp (P a0) u0@i) u1
+ <j>IdP (<i>P (p@j\/i)) (comp (<i>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) =