From ca9fa9fb3dd2ea34c2f204edc0d8f0483e021d9d Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 23 Apr 2015 17:26:25 +0200 Subject: [PATCH] Fix set --- examples/set.ctt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/set.ctt b/examples/set.ctt index 04607a6..67f0578 100644 --- 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 ( F (p@i)) u0 u1) : Id (IdP ( F (p@i)) u0 u1) q r = rem @ j @ i -- 2.34.1