bugfix in simplify, conv; extended prelude

diff --git a/Eval.hs b/Eval.hs
index bf127b08b7745df1dbe63082df159c396097ab0b..a1021c6d8fc470f43b31b760f986cd780638b223 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -140,7 +140,7 @@ eval rho v = case v of
   Snd a               -> sndVal (eval rho a)
   Where t decls       -> eval (Def decls rho) t
   Con name ts         -> VCon name (map (eval rho) ts)
-  PCon name a ts phi  -> 
+  PCon name a ts phi  ->
     pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi)
   Split{}             -> Ter v rho
   Sum{}               -> Ter v rho
@@ -295,15 +295,14 @@ trans i v0 v1 = case (v0,v1) of
     Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phi
     Nothing -> error $ "trans: missing path constructor " ++ c ++
                        " in " ++ show v0
+  (VGlue a ts,_)    -> transGlue i a ts v1
+  (VComp VU a es,_) -> transU i a es v1
   _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
   (Ter (Sum _ _ nass) env,VComp b w ws) -> comp k v01 (trans i v0 w) ws'
     where v01 = v0 `face` (i ~> 1)  -- b is vi0 and independent of j
           k   = fresh (v0,v1,Atom i)
           transp alpha w = trans i (v0 `face` alpha) (w @@ k)
           ws'          = mapWithKey transp ws
-
-  (VGlue a ts,_)    -> transGlue i a ts v1
-  (VComp VU a es,_) -> transU i a es v1
   _ | otherwise -> error $ "trans not implemented for v0 = " ++ show v0
                    ++ "\n and v1 = " ++ show v1
 
@@ -716,15 +715,15 @@ simplify :: Int -> Name -> Val -> Val
 simplify k j v = case v of
   VTrans p u | isIndep k j (p @@ j) -> simplify k j u
   VComp a u ts ->
-    let (ts',indep) = Map.partition (\t -> isIndep k j (t @@ j)) ts
+    let (indep,ts') = Map.partition (\t -> isIndep k j (t @@ j)) ts
     in if Map.null ts' then simplify k j u else VComp a u ts'
   VCompElem a es u us ->
-    let (es',indep) = Map.partition (\e -> isIndep k j (e @@ j)) es
+    let (indep,es') = Map.partition (\e -> isIndep k j (e @@ j)) es
         us'         = intersection us es'
     in if Map.null es' then simplify k j u else VCompElem a es' u us'
   VElimComp a es u ->
-    let (es',indep) = Map.partition (\e -> isIndep k j (e @@ j)) es
-        u' = simplify k j u
+    let (indep,es') = Map.partition (\e -> isIndep k j (e @@ j)) es
+        u'          = simplify k j u
     in if Map.null es' then u' else case u' of
       VCompElem _ _ w _ -> simplify k j w
       _ -> VElimComp a es' u'

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index da115404ca2ce8c93b9def8903ba0db9bd052008..f772009ad8e04247b14eb80610b89716289a29e5 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -68,3 +68,26 @@ constSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p =
       (i = 1) -> <k> p @ (j /\ k),
       (j = 0) -> <k> p @ (i \/ - k),
       (j = 1) -> <k> p @ (i /\ k)]
+
+prop (A : U) : U = (a b : A) -> Id A a b
+set (A : U) : U = (a b : A) -> prop (Id A a b)
+
+propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q =
+ <j i> comp A a [ (i=0) -> h a a
+                , (i=1) -> h a b
+                , (j=0) -> h a (p @ i)
+                , (j=1) -> h a (q @ i)]
+
+propIsProp (A : U) (f g : prop A) : Id (prop A) f g =
+ <i> \(a b :A) -> (propSet A f a b (f a b) (g a b)) @ i
+
+setIsProp (A : U) (f g : set A) : Id (set A) f g =
+ <i> \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i
+
+IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U =
+  IdP (<i> P (p @ i)) u0 u1
+
+lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A)
+         (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 =
+  <i> (pP (p @ i) (transport (<j> P (p @ i /\ j)) b0)
+          (transport (<j> P (p @ i \/ -j)) b1)) @ i
\ No newline at end of file