Finished eqToIso and removed constants for comp in U

diff --git a/CTT.hs b/CTT.hs
index 3dbe30cd86d2832addf9339631653164b2edbac9..1b8a68713ad602bbca42dddca8d4ef3f19062389 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -108,10 +108,6 @@ data Ter = App Ter Ter
            -- Kan composition and filling
          | Comp Ter Ter (System Ter)
          | Fill Ter Ter (System Ter)
-         -- | Trans Ter Ter
-           -- Composition in the Universe
-         -- | CompElem Ter (System Ter) Ter (System Ter)
-         -- | ElimComp Ter (System Ter) Ter
            -- Glue
          | Glue Ter (System Ter)
          | GlueElem Ter (System Ter)
@@ -156,9 +152,6 @@ data Val = VU
          | VGlue Val (System Val)
          | VGlueElem Val (System Val)
 
-           -- Composition in the universe (for now)
-         | VCompU Val (System Val)
-
            -- Composition for HITs; the type is constant
          | VHComp Val Val (System Val)
 
@@ -166,19 +159,13 @@ data Val = VU
          -- | VGlueLine Val Formula Formula
          -- | VGlueLineElem Val Formula Formula
 
-           -- Universe Composition Values
-         -- | VCompElem Val (System Val) Val (System Val)
-         -- | VElimComp Val (System Val) Val
-
            -- Neutral values:
          | VVar Ident Val
          | VFst Val
          | VSnd Val
            -- VUnGlueElem val type hisos
          | VUnGlueElem Val Val (System Val)
-         | VUnGlueElemU Val Val (System Val)
          | VSplit Val Val
-         -- | VHSqueeze Val Val Formula
          | VApp Val Val
          | VAppFormula Val Formula
          | VLam Ident Val Val
@@ -196,7 +183,6 @@ isNeutral v = case v of
   VApp{}         -> True
   VAppFormula{}  -> True
   VUnGlueElem{}  -> True
-  VUnGlueElemU{} -> True
   _              -> False
 
 isNeutralSystem :: System Val -> Bool
@@ -401,17 +387,12 @@ showTer v = case v of
   AppFormula e phi   -> showTer1 e <+> char '@' <+> showFormula phi
   Comp e t ts        -> text "comp" <+> showTers [e,t] <+> text (showSystem ts)
   Fill e t ts        -> text "fill" <+> showTers [e,t] <+> text (showSystem ts)
-  -- Trans e0 e1        -> text "transport" <+> showTers [e0,e1]
   Glue a ts          -> text "glue" <+> showTer1 a <+> text (showSystem ts)
   GlueElem a ts      -> text "glueElem" <+> showTer1 a <+> text (showSystem ts)
   -- GlueLine a phi psi -> text "glueLine" <+> showTer1 a <+>
   --                       showFormula phi <+> showFormula psi
   -- GlueLineElem a phi psi -> text "glueLineElem" <+> showTer1 a <+>
   --                           showFormula phi <+> showFormula psi
-  -- CompElem a es t ts -> text "compElem" <+> showTer1 a <+> text (showSystem es)
-  --                       <+> showTer1 t <+> text (showSystem ts)
-  -- ElimComp a es t    -> text "elimComp" <+> showTer1 a <+> text (showSystem es)
-  --                       <+> showTer1 t
 
 showTers :: [Ter] -> Doc
 showTers = hsep . map showTer1
@@ -446,7 +427,6 @@ showVal v = case v of
   VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us
                        <+> hsep (map ((char '@' <+>) . showFormula) phis)
   VHComp v0 v1 vs   -> text "hComp" <+> showVals [v0,v1] <+> text (showSystem vs)
-  -- VHSqueeze a u phi -> text "hSqueeze" <+> showVals [a,u] <+> showFormula phi
   VPi a l@(VLam x t b)
     | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b
     | otherwise          -> char '(' <> showLam v
@@ -462,23 +442,15 @@ showVal v = case v of
   VSnd u            -> showVal1 u <> text ".2"
   VUnGlueElem v b hs  -> text "unGlueElem" <+> showVals [v,b]
                          <+> text (showSystem hs)
-  VUnGlueElemU v b es -> text "unGlueElemU" <+> showVals [v,b]
-                         <+> text (showSystem es)
   VIdP v0 v1 v2     -> text "IdP" <+> showVals [v0,v1,v2]
   VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi
   VComp v0 v1 vs    -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
-  -- VTrans v0 v1      -> text "trans" <+> showVals [v0,v1]
   VGlue a ts        -> text "glue" <+> showVal1 a <+> text (showSystem ts)
   VGlueElem a ts    -> text "glueElem" <+> showVal1 a <+> text (showSystem ts)
-  VCompU a ts       -> text "compU" <+> showVal1 a <+> text (showSystem ts)
   -- VGlueLine a phi psi     -> text "glueLine" <+> showFormula phi
   --                            <+> showFormula psi  <+> showVal1 a
   -- VGlueLineElem a phi psi -> text "glueLineElem" <+> showFormula phi
   --                            <+> showFormula psi  <+> showVal1 a
-  -- VCompElem a es t ts -> text "compElem" <+> showVal1 a <+> text (showSystem es)
-  --                        <+> showVal1 t <+> text (showSystem ts)
-  -- VElimComp a es t    -> text "elimComp" <+> showVal1 a <+> text (showSystem es)
-  --                        <+> showVal1 t
 
 showPath :: Val -> Doc
 showPath e = case e of

diff --git a/Eval.hs b/Eval.hs
index 2aacdabf234b2adae5053f9adb9a4aa8efc4db78..7ffb0953447936247292540d8eca7f0b1f0585f8 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -64,9 +64,7 @@ instance Nominal Val where
     VSplit u v              -> support (u,v)
     VGlue a ts              -> support (a,ts)
     VGlueElem a ts          -> support (a,ts)
-    VCompU a ts             -> support (a,ts)
     VUnGlueElem a b hs      -> support (a,b,hs)
-    VUnGlueElemU a b es     -> support (a,b,es)
 
   act u (i, phi) | i `notElem` support u = u
                  | otherwise =
@@ -98,8 +96,6 @@ instance Nominal Val where
          VGlue a ts              -> glue (acti a) (acti ts)
          VGlueElem a ts          -> glueElem (acti a) (acti ts)
          VUnGlueElem a b hs      -> unGlue (acti a) (acti b) (acti hs)
-         VUnGlueElemU a b es     -> unGlueU (acti a) (acti b) (acti es)
-         VCompU a ts             -> compUniv (acti a) (acti ts)
 
   -- This increases efficiency as it won't trigger computation.
   swap u ij@(i,j) =
@@ -127,8 +123,7 @@ instance Nominal Val where
          VGlue a ts              -> VGlue (sw a) (sw ts)
          VGlueElem a ts          -> VGlueElem (sw a) (sw ts)
          VUnGlueElem a b hs      -> VUnGlueElem (sw a) (sw b) (sw hs)
-         VUnGlueElemU a b es     -> VUnGlueElemU (sw a) (sw b) (sw es)
-         VCompU a ts             -> VCompU (sw a) (sw ts)
+
 
 -----------------------------------------------------------------------
 -- The evaluator
@@ -247,7 +242,6 @@ inferType v = case v of
                   ++ ", got " ++ show ty
   VComp a _ _ -> a @@ One
   VUnGlueElem _ b hs  -> glue b hs
-  VUnGlueElemU _ b es -> compUniv b es
   _ -> error $ "inferType: not neutral " ++ show v
 
 (@@) :: ToFormula a => Val -> a -> Val
@@ -364,9 +358,7 @@ comp i a u ts = case a of
           ui1        = comp i a u1 t1s
           comp_u2    = comp i (app f fill_u1) u2 t2s
   VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts)
-  VU -> compUniv u (Map.map (VPath i) ts)
-        -- VGlue u (Map.map (eqToIso i) ts)
-  VCompU a es   -> compU i a es u ts
+  VU -> glue u (Map.map (eqToIso . VPath i) ts)
   VGlue b hisos -> compGlue i b hisos u ts
   Ter (Sum _ _ nass) env -> case u of
     VCon n us -> case lookupLabel n nass of
@@ -408,19 +400,35 @@ transpHIT i a u = squeezeHIT i a u `face` (i ~> 0)
 
 -- given u(i) of type a(i) "squeezeHIT i a u" connects in the direction i
 -- transHIT i a u(i=0) to u(i=1) in a(1)
-squeezeHIT :: Name -> Val -> Val -> Val
-squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of
-  VCon n us -> case lookupLabel n nass of
-    Just as -> VCon n (squeezes i as env us)
-    Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n
-  VPCon c _ ws0 phis -> case lookupLabel c nass of
-    Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) (phis `face` (i ~> 1))
-    Nothing -> error $ "squeezeHIT: missing path constructor " ++ c
-  VHComp _ v vs ->
-    hComp (a `face` (i ~> 1)) (transpHIT i a v) $
-      mapWithKey (\alpha vAlpha ->
-                   VPath i $ squeezeHIT i (a `face` alpha) (vAlpha @@ i)) vs
-  _ -> error $ "squeezeHIT: neutral " ++ show u
+-- squeezeHIT :: Name -> Val -> Val -> Val
+-- squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of
+--   VCon n us -> case lookupLabel n nass of
+--     Just as -> VCon n (squeezes i as env us)
+--     Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n
+--   VPCon c _ ws0 phis -> case lookupLabel c nass of
+--     Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) (phis `face` (i ~> 1))
+--     Nothing -> error $ "squeezeHIT: missing path constructor " ++ c
+--   VHComp _ v vs ->
+--     hComp (a `face` (i ~> 1)) (transpHIT i a v) $
+--       mapWithKey (\alpha vAlpha ->
+--                    VPath i $ squeezeHIT i (a `face` alpha) (vAlpha @@ i)) vs
+--   _ -> error $ "squeezeHIT: neutral " ++ show u
+squeezeHIT i a@(Ter (HSum _ _ nass) env) u =
+  let j = fresh (a,u)
+      aij = swap a (i,j)
+  in case u of
+   VCon n us -> case lookupLabel n nass of
+     Just as -> VCon n (squeezes i as env us)
+     Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n
+   VPCon c _ ws0 phis -> case lookupLabel c nass of
+     Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) phis
+     Nothing -> error $ "squeezeHIT: missing path constructor " ++ c
+   VHComp _ v vs ->
+     hComp (a `face` (i ~> 1)) (squeezeHIT i a v) $
+     mapWithKey (\alpha vAlpha ->
+                  VPath j $ squeezeHIT j (aij `face` alpha) (vAlpha @@ j)) vs
+   _ -> error $ "squeezeHIT: neutral " ++ show u
+
 
 hComp :: Val -> Val -> System Val -> Val
 hComp a u us | eps `Map.member` us = (us ! eps) @@ One
@@ -444,38 +452,32 @@ hisoFun :: Val -> Val
 hisoFun (VPair _ (VPair f _)) = f
 hisoFun x                     = error $ "HisoFun: Not an hiso: " ++ show x
 
--- -- Every line in the universe induces an hiso
+-- -- Every path in the universe induces an hiso
 eqToIso :: Val -> Val
-eqToIso e = VPair e0 (VPair f (VPair g (VPair s t)))
-  where e0 = e @@ Zero
+eqToIso e = VPair e1 (VPair f (VPair g (VPair s t)))
+  where e1 = e @@ One
         (i,j,x,y,ev) = (Name "i",Name "j",Var "x",Var "y",Var "E")
-        inv t = Path "i" $ AppFormula t (NegAtom i)
+        inv t = Path i $ AppFormula t (NegAtom i)
         evinv = inv ev
-        (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One))
-        eenv = upd ("E",e) empty
-        (eplus z,eminus z) = (Comp ev z Map.empty,Comp evinv z Map.empty)
-        -- NB: edown is not transNegFill
-        (eup z,edown z) = (Fill ev z Map.empty,Fill evinv z Map.empty)
-        f = Ter (Lam x ev1 (eminus x)) eenv
-        g = Ter (Lam y ev0 (eplus y)) eenv
-        -- s : (y : e0) -> f (g y) = y
-        ssys = mkSystem [(j ~> 0, inv (eup y)),
-                        ,(j ~> 1, edown (eplus y))]
-        s = Ter (Lam y ev0 $ Path j $ Comp einv (eplus y) ssys) eenv
-        -- t : (x : e1) -> g (f x) = x
-        -- tsys = mkSystem [(j ~> 0, eup (eup y)),
-        --                 ,(j ~> 1, edown (eplus y))]
-        -- t = Ter (Lam y ev0 $ Path j $ Comp einv (eplus y) ssys) eenv
-        -- t e a   = VPath j $ comp j (e @@ j) (transNeg j (e @@ j) a)
-        --             (mkSystem [(j ~> 0, transFill j (e @@ j)
-        --                                   (transNeg j (e @@ j) a))
-        --                       ,(j ~> 1, transFillNeg j (e @@ j) a)])
-
-
--- eqToIso :: Name -> Val -> Val
--- eqToIso i u = VPair a (VPair f (VPair g (VPair s t)))
---   where a = u `face` (i ~> 1)
---         f = Ter (Lam "x" (Var "A") (Transport )) (upd ("A",a) empty)
+        (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a)
+        eenv     = upd ("E",e) empty
+        -- eplus : e0 -> e1
+        eplus z  = Comp ev z Map.empty
+        -- eminus : e1 -> e0
+        eminus z = Comp evinv z Map.empty
+        -- NB: edown is *not* transNegFill
+        eup z   = Fill ev z Map.empty
+        edown z = Fill evinv z Map.empty
+        f = Ter (Lam "x" ev1 (eminus x)) eenv
+        g = Ter (Lam "y" ev0 (eplus y)) eenv
+        -- s : (y : e0) -> eminus (eplus y) = y
+        ssys = mkSystem [(j ~> 1, inv (eup y))
+                        ,(j ~> 0, edown (eplus y))]
+        s = Ter (Lam "y" ev0 $ Path j $ Comp evinv (eplus y) ssys) eenv
+        -- t : (x : e1) -> eplus (eminus x) = x
+        tsys = mkSystem [(j ~> 0, eup (eminus x))
+                        ,(j ~> 1, inv (edown x))]
+        t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv
 
 glue :: Val -> System Val -> Val
 glue b ts | Map.null ts         = b
@@ -580,110 +582,6 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v =
         theta'' = comp j b (app f theta') xs
 
 
--------------------------------------------------------------------------------
--- | Composition in the Universe (to be replaced as glue)
-
-unGlueU :: Val -> Val -> System Val -> Val
-unGlueU w b es
-    | Map.null es         = w
-    | eps `Map.member` es = transNegLine (es ! eps) w
-    | otherwise           = case w of
-       VGlueElem v us   -> v
-       _ -> VUnGlueElemU w b es
-
-compUniv :: Val -> System Val -> Val
-compUniv b es | Map.null es         = b
-              | eps `Map.member` es = (es ! eps) @@ One
-              | otherwise           = VCompU b es
-
-
-compU :: Name -> Val -> System Val -> Val -> System Val -> Val
-compU i b es wi0 ws = glueElem vi1'' usi1''
-  where bi1 = b `face` (i ~> 1)
-        vs   = mapWithKey (\alpha wAlpha ->
-                 unGlueU wAlpha (b `face` alpha) (es `face` alpha)) ws
-        vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs
-        vi0  = unGlueU wi0 (b `face` (i ~> 0)) (es `face` (i ~> 0)) -- in b(i0)
-
-        v    = fill i b vi0 vs           -- in b
-        vi1  = comp i b vi0 vs           -- is v `face` (i ~> 1) in b(i1)
-
-        esI1 = es `face` (i ~> 1)
-        es'  = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es
-        es'' = filterWithKey (\alpha _ -> not (alpha `Map.member` es')) esI1
-
-        us'    = mapWithKey (\gamma eGamma ->
-                   fill i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma))
-                 es'
-        usi1'  = mapWithKey (\gamma eGamma ->
-                   comp i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma))
-                 es'
-
-        ls'    = mapWithKey (\gamma eGamma ->
-                     pathComp i (b `face` gamma) (v `face` gamma)
-                       (transNegLine eGamma (us' ! gamma)) (vs `face` gamma))
-                   es'
-
-        vi1' = compLine (constPath bi1) vi1
-                 (ls' `unionSystem` Map.map constPath vsi1)
-
-        wsi1 = ws `face` (i ~> 1)
-
-        -- for gamma in es'', (i1) gamma is in es, so wsi1 gamma
-        -- is in the domain of isoGamma
-        uls'' = mapWithKey (\gamma eGamma ->
-                  gradLemmaU (bi1 `face` gamma) eGamma
-                    ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma))
-                    (vi1' `face` gamma))
-                  es''
-
-
-        vsi1' = Map.map constPath $ border vi1' es' `unionSystem` vsi1
-
-        vi1'' = compLine (constPath bi1) vi1'
-                  (Map.map snd uls'' `unionSystem` vsi1')
-
-        usi1'' = Map.mapWithKey (\gamma _ ->
-                     if gamma `Map.member` usi1' then usi1' ! gamma
-                     else fst (uls'' ! gamma))
-                   esI1
-
-
--- Grad Lemma, takes a line eq in U, a system us and a value v, s.t. f us =
--- border v. Outputs (u,p) s.t. border u = us and a path p between v
--- and f u, where f is transNegLine eq
-gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val)
-gradLemmaU b eq us v = (u, VPath i theta'')
-  where i:j:_   = freshs (b,eq,us,v)
-        a       = eq @@ One
-        g       = transLine
-        f       = transNegLine
-        s e b   = VPath j $ compNeg j (e @@ j) (trans j (e @@ j) b)
-                    (mkSystem [(j ~> 0, transFill j (e @@ j) b)
-                              ,(j ~> 1, transFillNeg j (e @@ j)
-                                          (trans j (e @@ j) b))])
-        t e a   = VPath j $ comp j (e @@ j) (transNeg j (e @@ j) a)
-                    (mkSystem [(j ~> 0, transFill j (e @@ j)
-                                          (transNeg j (e @@ j) a))
-                              ,(j ~> 1, transFillNeg j (e @@ j) a)])
-        gv      = g eq v
-        us'     = mapWithKey (\alpha uAlpha ->
-                                   t (eq `face` alpha) uAlpha @@ i) us
-        theta   = fill i a gv us'
-        u       = comp i a gv us'  -- Same as "theta `face` (i ~> 1)"
-        ws      = insertSystem (i ~> 0) gv $
-                  insertSystem (i ~> 1) (t eq u @@ j) $
-                  mapWithKey
-                    (\alpha uAlpha ->
-                      t (eq `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us
-        theta'  = compNeg j a theta ws
-        xs      = insertSystem (i ~> 0) (s eq v @@ j) $
-                  insertSystem (i ~> 1) (s eq (f eq u) @@ j) $
-                  mapWithKey
-                    (\alpha uAlpha ->
-                       s (eq `face` alpha) (f (eq `face` alpha) uAlpha) @@ j) us
-        theta'' = comp j b (f eq theta') xs
-
 -------------------------------------------------------------------------------
 -- | Conversion
 
@@ -741,7 +639,6 @@ instance Convertible Val where
       (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos')
       (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us')
       (VUnGlueElem u _ _,VUnGlueElem u' _ _) -> conv ns u u'
-      (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'
       _                         -> False
 
 instance Convertible Ctxt where
@@ -797,8 +694,6 @@ instance Normal Val where
     VGlue u hisos       -> glue (normal ns u) (normal ns hisos)
     VGlueElem u us      -> glueElem (normal ns u) (normal ns us)
     VUnGlueElem u b hs  -> unGlue (normal ns u) (normal ns b) (normal ns hs)
-    VUnGlueElemU u b es -> unGlueU (normal ns u) (normal ns b) (normal ns es)
-    VCompU u es         -> compUniv (normal ns u) (normal ns es)
     VVar x t            -> VVar x t -- (normal ns t)
     VFst t              -> fstVal (normal ns t)
     VSnd t              -> sndVal (normal ns t)

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 82f51bf331472626d1b5daa82ea0971214d8f843..aa5331670640d802798eb3764ee6901ad9152016 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -191,7 +191,9 @@ check a t = case (a,t) of
     ns <- asks names\r
     rho <- asks env\r
     unlessM (a === eval rho a') $\r
-      throwError "check: lam types don't match"\r
+      throwError $ "check: lam types don't match"\r
+        ++ "\nlambda type annotation: " ++ show a'\r
+        ++ "\ndomain of Pi: " ++ show a\r
     let var = mkVarNice ns x a\r
     local (addTypeVal (x,a)) $ check (app f var) t\r
   (VSigma a f, Pair t1 t2) -> do\r

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 8825eea028855e69fa8ba3a701f2cac049b56132..9dcc6ba72ab07bfcba9182f2d2634b21d55a3267 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -83,5 +83,5 @@ test8 : Id U F2 F2 =
 test9 : Id U F2 F2 =
   transport (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool)
 
-p : Id U F2 bool = <i> comp U bool [ (i = 0) -> boolEqF2 ]
+p : Id U F2 bool = <i> comp (<_>U) bool [ (i = 0) -> boolEqF2 ]
 q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file

diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
index eae59dfa97965d9fadc98e917ae814d8e3ebf59d..03bb539a1dedc46b39ea1fb6205a5584700b788a 100644 (file)
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -8,7 +8,7 @@ hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b)
     (<i>(f a (refl A a)))\r
 \r
 hedberg (A:U) (a b:A) (h: (x:A) -> stable (Id A a x)) (p q : Id A a b) : Id (Id A a b) p q =\r
- <j i>comp A a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j]\r
+ <j i>comp (<_> A) a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j]\r
  where \r
    ra : Id A a a = refl A a \r
    rem1 (x:A) : exConst (Id A a x) = stableConst (Id A a x) (h x)\r

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 925118259476f9b066cb53b57cbf4282ba0fd556..ce3b7e7a624fdf8d29a5d6d62b268a1e47164b89 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -41,7 +41,7 @@ J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
 inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 
 compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
-  <i> comp A (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ]
+  <i> comp (<_>A) (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ]
 
 compId' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
   subst A (Id A a) b c q p
@@ -52,7 +52,7 @@ compId'' (A : U) (a b : A) (p : Id A a b) : (c : A) -> (q : Id A b c) -> Id A a
 
 compUp (A : U) (a a' b b' : A)
        (p : Id A a a') (q : Id A b b') (r : Id A a b) : Id A a' b' =
-  <i> comp A (r @ i) [(i = 0) -> p, (i = 1) -> q]
+  <i> comp (<_>A) (r @ i) [(i = 0) -> p, (i = 1) -> q]
 
 compDown (A : U) (a a' b b' : A)
          (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b =
@@ -72,7 +72,7 @@ test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
 
 kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
                           (r : Id A b d) : Id A c d =
-  <i> comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
+  <i> comp (<_>A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
 
 -- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
 --           (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
@@ -107,7 +107,7 @@ Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
   = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1
 
 constSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p =
-  <i j> comp A a
+  <i j> comp (<_>A) a
      [(i = 0) -> <k> p @ (j \/ - k),
       (i = 1) -> <k> p @ (j /\ k),
       (j = 0) -> <k> p @ (i \/ - k),
@@ -118,7 +118,7 @@ set (A : U) : U = (a b : A) -> prop (Id A a b)
 groupoid (A : U) : U = (a b : A) -> set (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
+ <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)]