projects
/
cubicaltt.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
53de597
)
Fix set
author
Anders
<mortberg@chalmers.se>
Thu, 23 Apr 2015 15:26:25 +0000
(17:26 +0200)
committer
Anders
<mortberg@chalmers.se>
Thu, 23 Apr 2015 15:26:25 +0000
(17:26 +0200)
examples/set.ctt
patch
|
blob
|
blame
|
history
diff --git
a/examples/set.ctt
b/examples/set.ctt
index 04607a6307d8a49bf861e8d08642424588499ad6..67f0578e573d9ed8235a5eb60995d197e9387a56 100644
(file)
--- a/
examples/set.ctt
+++ b/
examples/set.ctt
@@
-1,5
+1,7
@@
module set where
+import prelude
+
sqDepPath (A:U) (F:A->U) (sF:(x:A) -> set (F x))
(a0 a1:A) (p:Id A a0 a1) (u0 : F a0) (u1 : F a1) (q r: IdP (<i> F (p@i)) u0 u1) :
Id (IdP (<i> F (p@i)) u0 u1) q r = <i j> rem @ j @ i