From: Simon Huber <hubsim@gmail.com>
Date: Tue, 2 Jun 2015 13:03:56 +0000 (+0200)
Subject: Started adapting for the non-regular setting (wip)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7ad3c515569e7b6ff1f551100253b4b916f8c03f;p=cubicaltt.git

Started adapting for the non-regular setting (wip)
---

diff --git a/CTT.hs b/CTT.hs
index 0d86209..b3bc093 100644
--- a/CTT.hs
+++ b/CTT.hs
@@ -106,16 +106,16 @@ data Ter = App Ter Ter
          | AppFormula Ter Formula
            -- Kan Composition
          | Comp Ter Ter (System Ter)
-         | Trans Ter Ter
+         -- | Trans Ter Ter
            -- Composition in the Universe
-         | CompElem Ter (System Ter) Ter (System Ter)
-         | ElimComp Ter (System Ter) Ter
+         -- | CompElem Ter (System Ter) Ter (System Ter)
+         -- | ElimComp Ter (System Ter) Ter
            -- Glue
          | Glue Ter (System Ter)
          | GlueElem Ter (System Ter)
            -- GlueLine: connecting any type to its glue with identities
-         | GlueLine Ter Formula Formula
-         | GlueLineElem Ter Formula Formula
+         -- | GlueLine Ter Formula Formula
+         -- | GlueLineElem Ter Formula Formula
   deriving Eq
 
 -- For an expression t, returns (u,ts) where u is no application and t = u ts
@@ -148,19 +148,19 @@ data Val = VU
          | VIdP Val Val Val
          | VPath Name Val
          | VComp Val Val (System Val)
-         | VTrans Val Val
+         -- | VTrans Val Val
 
            -- Glue values
          | VGlue Val (System Val)
          | VGlueElem Val (System Val)
 
            -- GlueLine values
-         | VGlueLine Val Formula Formula
-         | VGlueLineElem Val Formula Formula
+         -- | VGlueLine Val Formula Formula
+         -- | VGlueLineElem Val Formula Formula
 
            -- Universe Composition Values
-         | VCompElem Val (System Val) Val (System Val)
-         | VElimComp Val (System Val) Val
+         -- | VCompElem Val (System Val) Val (System Val)
+         -- | VElimComp Val (System Val) Val
 
            -- Neutral values:
          | VVar Ident Val
@@ -172,6 +172,15 @@ data Val = VU
          | VLam Ident Val Val
   deriving Eq
 
+-- data HIso = Iso Val Val Val Val Val
+--           | Eq Val
+--   deriving (Eq,Show)
+
+-- toHIso :: Val -> HIso
+-- toHIso (VPair a (VPair f (VPair g (VPair s t)))) = Iso a f g s t
+-- toHIso v = Eq v
+-- toHIso _ = error "toHIso"
+
 isNeutral :: Val -> Bool
 isNeutral v = case v of
   Ter Undef{} _     -> True
@@ -183,9 +192,9 @@ isNeutral v = case v of
   VApp v _          -> isNeutral v
   VAppFormula v _   -> isNeutral v
   VComp a u ts      -> isNeutralComp a u ts
-  VTrans a u        -> isNeutralTrans a u
-  VCompElem _ _ u _ -> isNeutral u
-  VElimComp _ _ u   -> isNeutral u
+  -- VTrans a u        -> isNeutralTrans a u
+  -- VCompElem _ _ u _ -> isNeutral u
+  -- VElimComp _ _ u   -> isNeutral u
   _                 -> False
 
 isNeutralSystem :: System Val -> Bool
@@ -195,18 +204,19 @@ isNeutralPath :: Val -> Bool
 isNeutralPath (VPath _ v) = isNeutral v
 isNeutralPath _ = True
 
-isNeutralTrans :: Val -> Val -> Bool
-isNeutralTrans (VPath i a) u = foo i a u
-  where foo :: Name -> Val -> Val -> Bool
-        foo i a u | isNeutral a = True
-        foo i (Ter Sum{} _) u   = isNeutral u
-        foo i (VGlue _ as) u    =
-          let shasBeta = shape as `face` (i ~> 0)
-          in shasBeta /= Map.empty && eps `Map.notMember` shasBeta && isNeutral u
-        foo _ _ _ = False
--- TODO: case for VGLueLine
-isNeutralTrans u _ = isNeutral u
-
+-- isNeutralTrans :: Val -> Val -> Bool
+-- isNeutralTrans (VPath i a) u = foo i a u
+--   where foo :: Name -> Val -> Val -> Bool
+--         foo i a u | isNeutral a = True
+--         foo i (Ter Sum{} _) u   = isNeutral u
+--         foo i (VGlue _ as) u    =
+--           let shasBeta = shape as `face` (i ~> 0)
+--           in shasBeta /= Map.empty && eps `Map.notMember` shasBeta && isNeutral u
+--         foo _ _ _ = False
+-- -- TODO: case for VGLueLine
+-- isNeutralTrans u _ = isNeutral u
+
+-- TODO: adapt for non-regular setting
 isNeutralComp :: Val -> Val -> System Val -> Bool
 isNeutralComp a _ _ | isNeutral a = True
 isNeutralComp (Ter Sum{} _) u ts  = isNeutral u || isNeutralSystem ts
@@ -368,17 +378,17 @@ showTer v = case v of
   AppFormula e phi   -> showTer1 e <+> char '@' <+> showFormula phi
   Comp e0 e1 es      -> text "comp" <+> showTers [e0,e1]
                         <+> text (showSystem es)
-  Trans e0 e1        -> text "transport" <+> showTers [e0,e1]
+  -- 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
+  -- 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
@@ -426,17 +436,17 @@ showVal v = case v of
   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]
+  -- 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)
-  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
+  -- 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 594e9bb..0e958ed 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -42,6 +42,17 @@ instance Nominal Ctxt where
   act e _   = e
   swap e _  = e
 
+instance Nominal HIso where
+  support h = case h of
+    Iso a f g s t -> support [a,f,g,s,t]
+    Eq v -> support v
+  act h iphi = case h of
+    Iso a f g s t -> Iso (a `act` iphi) (f `act` iphi) (g `act` iphi) (s `act` iphi) (t `act` iphi)
+    Eq v -> Eq (v `act` iphi)
+  swap h ij = case h of
+    Iso a f g s t -> Iso (a `swap` ij) (f`swap` ij) (g`swap` ij) (s`swap` ij) (t`swap` ij)
+    Eq v -> Eq (v`swap` ij)
+
 instance Nominal Val where
   support v = case v of
     VU                      -> []
@@ -50,7 +61,7 @@ instance Nominal Val where
     VComp a u ts            -> support (a,u,ts)
     VIdP a v0 v1            -> support [a,v0,v1]
     VPath i v               -> i `delete` support v
-    VTrans u v              -> support (u,v)
+    -- VTrans u v              -> support (u,v)
     VSigma u v              -> support (u,v)
     VPair u v               -> support (u,v)
     VFst u                  -> support u
@@ -64,10 +75,10 @@ instance Nominal Val where
     VSplit u v              -> support (u,v)
     VGlue a ts              -> support (a,ts)
     VGlueElem a ts          -> support (a,ts)
-    VGlueLine a phi psi     -> support (a,phi,psi)
-    VGlueLineElem a phi psi -> support (a,phi,psi)
-    VCompElem a es u us     -> support (a,es,u,us)
-    VElimComp a es u        -> support (a,es,u)
+    -- VGlueLine a phi psi     -> support (a,phi,psi)
+    -- VGlueLineElem a phi psi -> support (a,phi,psi)
+    -- VCompElem a es u us     -> support (a,es,u,us)
+    -- VElimComp a es u        -> support (a,es,u)
 
   act u (i, phi) | i `notElem` support u = u
                  | otherwise =
@@ -84,7 +95,7 @@ instance Nominal Val where
                    | j `notElem` sphi -> VPath j (acti v)
                    | otherwise -> VPath k (acti (v `swap` (j,k)))
               where k = fresh (v,Atom i,phi)
-         VTrans u v              -> transLine (acti u) (acti v)
+         -- VTrans u v              -> transLine (acti u) (acti v)
          VSigma a f              -> VSigma (acti a) (acti f)
          VPair u v               -> VPair (acti u) (acti v)
          VFst u                  -> fstVal (acti u)
@@ -98,10 +109,10 @@ instance Nominal Val where
          VSplit u v              -> app (acti u) (acti v)
          VGlue a ts              -> glue (acti a) (acti ts)
          VGlueElem a ts          -> glueElem (acti a) (acti ts)
-         VGlueLine a phi psi     -> glueLine (acti a) (acti phi) (acti psi)
-         VGlueLineElem a phi psi -> glueLineElem (acti a) (acti phi) (acti psi)
-         VCompElem a es u us     -> compElem (acti a) (acti es) (acti u) (acti us)
-         VElimComp a es u        -> elimComp (acti a) (acti es) (acti u)
+         -- VGlueLine a phi psi     -> glueLine (acti a) (acti phi) (acti psi)
+         -- VGlueLineElem a phi psi -> glueLineElem (acti a) (acti phi) (acti psi)
+         -- VCompElem a es u us     -> compElem (acti a) (acti es) (acti u) (acti us)
+         -- VElimComp a es u        -> elimComp (acti a) (acti es) (acti u)
 
   -- This increases efficiency as it won't trigger computation.
   swap u ij@(i,j) =
@@ -114,7 +125,7 @@ instance Nominal Val where
          VComp a v ts            -> VComp (sw a) (sw v) (sw ts)
          VIdP a u v              -> VIdP (sw a) (sw u) (sw v)
          VPath k v               -> VPath (swapName k ij) (sw v)
-         VTrans u v              -> VTrans (sw u) (sw v)
+         -- VTrans u v              -> VTrans (sw u) (sw v)
          VSigma a f              -> VSigma (sw a) (sw f)
          VPair u v               -> VPair (sw u) (sw v)
          VFst u                  -> VFst (sw u)
@@ -128,10 +139,10 @@ instance Nominal Val where
          VSplit u v              -> VSplit (sw u) (sw v)
          VGlue a ts              -> VGlue (sw a) (sw ts)
          VGlueElem a ts          -> VGlueElem (sw a) (sw ts)
-         VGlueLine a phi psi     -> VGlueLine (sw a) (sw phi) (sw psi)
-         VGlueLineElem a phi psi -> VGlueLineElem (sw a) (sw phi) (sw psi)
-         VCompElem a es u us     -> VCompElem (sw a) (sw es) (sw u) (sw us)
-         VElimComp a es u        -> VElimComp (sw a) (sw es) (sw u)
+         -- VGlueLine a phi psi     -> VGlueLine (sw a) (sw phi) (sw psi)
+         -- VGlueLineElem a phi psi -> VGlueLineElem (sw a) (sw phi) (sw psi)
+         -- VCompElem a es u us     -> VCompElem (sw a) (sw es) (sw u) (sw us)
+         -- VElimComp a es u        -> VElimComp (sw a) (sw es) (sw u)
 
 -----------------------------------------------------------------------
 -- The evaluator
@@ -159,18 +170,18 @@ eval rho v = case v of
   Path i t            ->
     let j = fresh rho
     in VPath j (eval (sub (i,Atom j) rho) t)
-  Trans u v           -> transLine (eval rho u) (eval rho v)
+  -- Trans u v           -> transLine (eval rho u) (eval rho v)
   AppFormula e phi    -> eval rho e @@ evalFormula rho phi
   Comp a t0 ts        -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts)
   Glue a ts           -> glue (eval rho a) (evalSystem rho ts)
   GlueElem a ts       -> glueElem (eval rho a) (evalSystem rho ts)
-  GlueLine a phi psi  ->
-    glueLine (eval rho a) (evalFormula rho phi) (evalFormula rho psi)
-  GlueLineElem a phi psi ->
-    glueLineElem (eval rho a) (evalFormula rho phi) (evalFormula rho psi)
-  CompElem a es u us  -> compElem (eval rho a) (evalSystem rho es) (eval rho u)
-                                  (evalSystem rho us)
-  ElimComp a es u     -> elimComp (eval rho a) (evalSystem rho es) (eval rho u)
+  -- GlueLine a phi psi  ->
+  --   glueLine (eval rho a) (evalFormula rho phi) (evalFormula rho psi)
+  -- GlueLineElem a phi psi ->
+  --   glueLineElem (eval rho a) (evalFormula rho phi) (evalFormula rho psi)
+  -- CompElem a es u us  -> compElem (eval rho a) (evalSystem rho es) (eval rho u)
+  --                                 (evalSystem rho us)
+  -- ElimComp a es u     -> elimComp (eval rho a) (evalSystem rho es) (eval rho u)
   _                   -> error $ "Cannot evaluate " ++ show v
 
 evalFormula :: Env -> Formula -> Formula
@@ -206,36 +217,40 @@ app u v = case (u,v) of
                    wsj = Map.map (@@ j) ws
                    w'  = app u w
                    ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj
-               in genComp j (app f (fill j a w wsj)) w' ws'
+                   -- a should be constant
+               in comp j (app f (fill j (a @@ j) w wsj)) w' ws'
     _ -> error $ "app: Split annotation not a Pi type " ++ show u
   (Ter Split{} _,_) | isNeutral v         -> VSplit u v
-  (Ter Split{} _,VCompElem _ _ w _)       -> app u w
-  (Ter Split{} _,VElimComp _ _ w)         -> app u w
-  (VTrans (VPath i (VPi a f)) li0,vi1) ->
-    let j       = fresh (u,vi1)
+  -- (Ter Split{} _,VCompElem _ _ w _)       -> app u w
+  -- (Ter Split{} _,VElimComp _ _ w)         -> app u w
+  -- (VTrans (VPath i (VPi a f)) li0,vi1) ->
+  --   let j       = fresh (u,vi1)
+  --       (aj,fj) = (a,f) `swap` (i,j)
+  --       v       = transFillNeg j aj vi1
+  --       vi0     = transNeg j aj vi1
+  --   in trans j (app fj v) (app li0 vi0)
+  (VComp (VPath i (VPi a f)) li0 ts,vi1) ->
+    let j   = fresh (u,vi1)
         (aj,fj) = (a,f) `swap` (i,j)
+        tsj = Map.map (@@ j) ts
         v       = transFillNeg j aj vi1
         vi0     = transNeg j aj vi1
-    in trans j (app fj v) (app li0 vi0)
-  (VComp (VPi a f) li0 ts,vi1) ->
-    let j   = fresh (u,vi1)
-        tsj = Map.map (@@ j) ts
-    in comp j (app f vi1) (app li0 vi1)
-              (intersectionWith app tsj (border vi1 tsj))
+    in comp j (app fj v) (app li0 vi0)
+              (intersectionWith app tsj (border v tsj))
   _ | isNeutral u       -> VApp u v
-  (VCompElem _ _ u _,_) -> app u v
-  (VElimComp _ _ u,_)   -> app u v
+  -- (VCompElem _ _ u _,_) -> app u v
+  -- (VElimComp _ _ u,_)   -> app u v
   _                     -> error $ "app \n  " ++ show u ++ "\n  " ++ show v
 
 fstVal, sndVal :: Val -> Val
 fstVal (VPair a b)     = a
-fstVal (VElimComp _ _ u) = fstVal u
-fstVal (VCompElem _ _ u _) = fstVal u
+-- fstVal (VElimComp _ _ u) = fstVal u
+-- fstVal (VCompElem _ _ u _) = fstVal u
 fstVal u | isNeutral u = VFst u
 fstVal u               = error $ "fstVal: " ++ show u ++ " is not neutral."
 sndVal (VPair a b)     = b
-sndVal (VElimComp _ _ u) = sndVal u
-sndVal (VCompElem _ _ u _) = sndVal u
+-- sndVal (VElimComp _ _ u) = sndVal u
+-- sndVal (VCompElem _ _ u _) = sndVal u
 sndVal u | isNeutral u = VSnd u
 sndVal u               = error $ "sndVal: " ++ show u ++ " is not neutral."
 
@@ -264,8 +279,8 @@ inferType v = case v of
     VIdP a _ _ -> a @@ phi
     ty         -> error $ "inferType: expected IdP type for " ++ show v
                   ++ ", got " ++ show ty
-  VComp a _ _ -> a
-  VTrans a _  -> a @@ One
+  VComp a _ _ -> a @@ One
+--  VTrans a _  -> a @@ One
   _ -> error $ "inferType: not neutral " ++ show v
 
 (@@) :: ToFormula a => Val -> a -> Val
@@ -275,13 +290,12 @@ v @@ phi | isNeutral v     = case (inferType v,toFormula phi) of
   (VIdP  _ a0 _,Dir 0) -> a0
   (VIdP  _ _ a1,Dir 1) -> a1
   _  -> VAppFormula v (toFormula phi)
-(VCompElem _ _ u _) @@ phi = u @@ phi
-(VElimComp _ _ u) @@ phi   = u @@ phi
+-- (VCompElem _ _ u _) @@ phi = u @@ phi
+-- (VElimComp _ _ u) @@ phi   = u @@ phi
 v @@ phi                   = error $ "(@@): " ++ show v ++ " should be neutral."
 
 pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val
 pcon c a@(Ter (Sum _ _ lbls) rho) us phis = case lookupPLabel c lbls of
-  -- TODO: is this correct? Double check!
   Just (tele,is,ts) | eps `Map.member` vs -> vs ! eps
                     | otherwise -> VPCon c a us phis
     where rho' = subs (zip is phis) (updsTele tele us rho)
@@ -301,48 +315,48 @@ transNegLine u v = transNeg i (u @@ i) v
   where i = fresh (u,v)
 
 trans :: Name -> Val -> Val -> Val
-trans i v0 v1 | i `notElem` support v0 = v1
-trans i v0 v1 = case (v0,v1) of
-  (VIdP a u v,w) ->
-    let j   = fresh (Atom i,v0,w)
-        ts' = mkSystem [(j ~> 0,u),(j ~> 1,v)]
-    in VPath j $ genComp i (a @@ j) (w @@ j) ts'
-  (VSigma a f,u) ->
-    let (u1,u2) = (fstVal u,sndVal u)
-        fill_u1 = transFill i a u1
-        ui1     = trans i a u1
-        comp_u2 = trans i (app f fill_u1) u2
-    in VPair ui1 comp_u2
-  (VPi{},_) -> VTrans (VPath i v0) v1
-  (Ter (Sum _ _ nass) env,VCon c us) -> case lookupLabel c nass of
-    Just as -> VCon c $ transps i as env us
-    Nothing -> error $ "trans: missing constructor " ++ c ++ " in " ++ show v0
-  (Ter (Sum _ _ nass) env,VPCon c _ ws0 phis) -> case lookupLabel c nass of
-    -- v1 should be independent of i, so i # phi
-    Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phis
-    Nothing -> error $ "trans: missing path constructor " ++ c ++
-                       " in " ++ show v0
-  _ | isNeutral w -> w
-    where w = VTrans (VPath i v0) v1
-  (Ter (Sum _ _ nass) env,VElimComp _ _ u) -> trans i v0 u
-  (Ter (Sum _ _ nass) env,VCompElem _ _ u _) -> trans i v0 u
-  (VGlue a ts,_)    -> transGlue i a ts v1
-  (VGlueLine a phi psi,_) -> transGlueLine i a phi psi v1
-  (VComp VU a es,_) -> transU i a es 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
-  _ -> error $ "trans not implemented for v0 = " ++ show v0
-            ++ "\n and v1 = " ++ show v1
+trans i v0 v1 = comp i v0 v1 Map.empty
+-- trans i v0 v1 | i `notElem` support v0 = v1
+-- trans i v0 v1 = case (v0,v1) of
+--   (VIdP a u v,w) ->
+--     let j   = fresh (Atom i,v0,w)
+--         ts' = mkSystem [(j ~> 0,u),(j ~> 1,v)]
+--     in VPath j $ comp i (a @@ j) (w @@ j) ts'
+--   (VSigma a f,u) ->
+--     let (u1,u2) = (fstVal u,sndVal u)
+--         fill_u1 = transFill i a u1
+--         ui1     = trans i a u1
+--         comp_u2 = trans i (app f fill_u1) u2
+--     in VPair ui1 comp_u2
+--   (VPi{},_) -> VTrans (VPath i v0) v1
+--   (Ter (Sum _ _ nass) env,VCon c us) -> case lookupLabel c nass of
+--     Just as -> VCon c $ transps i as env us
+--     Nothing -> error $ "trans: missing constructor " ++ c ++ " in " ++ show v0
+--   (Ter (Sum _ _ nass) env,VPCon c _ ws0 phis) -> case lookupLabel c nass of
+--     -- v1 should be independent of i, so i # phi
+--     Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phis
+--     Nothing -> error $ "trans: missing path constructor " ++ c ++
+--                        " in " ++ show v0
+--   _ | isNeutral w -> w
+--     where w = VTrans (VPath i v0) v1
+--   (Ter (Sum _ _ nass) env,VElimComp _ _ u) -> trans i v0 u
+--   (Ter (Sum _ _ nass) env,VCompElem _ _ u _) -> trans i v0 u
+--   (VGlue a ts,_)    -> transGlue i a ts v1
+--   (VGlueLine a phi psi,_) -> transGlueLine i a phi psi v1
+--   (VComp VU a es,_) -> transU i a es 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
+--   _ -> error $ "trans not implemented for v0 = " ++ show v0
+--             ++ "\n and v1 = " ++ show v1
 
 transNeg :: Name -> Val -> Val -> Val
 transNeg i a u = trans i (a `sym` i) u
 
 transFill, transFillNeg :: Name -> Val -> Val -> Val
-transFill i a u = trans j (a `conj` (i,j)) u
-  where j = fresh (Atom i,a,u)
+transFill i a u = fill i a u Map.empty
 transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i
 
 transps :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val]
@@ -357,97 +371,111 @@ transps _ _ _ _ = error "transps: different lengths of types and values"
 -- Given u of type a "squeeze i a u" connects in the direction i
 -- trans i a u(i=0) to u(i=1)
 squeeze :: Name -> Val -> Val -> Val
-squeeze i a u = trans j (a `disj` (i,j)) u
+squeeze i a u = comp i a ui0 $ mkSystem [ (j ~> 0, transFill i a ui0)
+                                        , (j ~> 1, u) ]
   where j = fresh (Atom i,a,u)
+        ui0 = u `face` (i ~> 0)
 
-squeezeNeg :: Name -> Val -> Val -> Val
-squeezeNeg i a u = transNeg j (a `conj` (i,j)) u
-  where j = fresh (Atom i,a,u)
+-- squeezeNeg :: Name -> Val -> Val -> Val
+-- squeezeNeg i a u = transNeg j (a `conj` (i,j)) u
+--   where j = fresh (Atom i,a,u)
 
 -------------------------------------------------------------------------------
 -- Composition
 
 compLine :: Val -> Val -> System Val -> Val
-compLine a u ts = comp i a u (Map.map (@@ i) ts)
+compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts)
   where i = fresh (a,u,ts)
 
-genComp, genCompNeg :: Name -> Val -> Val -> System Val -> Val
-genComp i a u ts | Map.null ts = trans i a u
-genComp i a u ts = comp i ai1 (trans i a u) ts'
-  where ai1 = a `face` (i ~> 1)
-        ts' = mapWithKey (\alpha -> squeeze i (a `face` alpha)) ts
-genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i)
+-- genComp, genCompNeg :: Name -> Val -> Val -> System Val -> Val
+-- genComp i a u ts | Map.null ts = trans i a u
+-- genComp i a u ts = comp i ai1 (trans i a u) ts'
+--   where ai1 = a `face` (i ~> 1)
+--         ts' = mapWithKey (\alpha -> squeeze i (a `face` alpha)) ts
+-- genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i)
 
 fillLine :: Val -> Val -> System Val -> Val
-fillLine a u ts = VPath i $ fill i a u (Map.map (@@ i) ts)
+fillLine a u ts = VPath i $ fill i (a @@ i) u (Map.map (@@ i) ts)
   where i = fresh (a,u,ts)
 
 fill, fillNeg :: Name -> Val -> Val -> System Val -> Val
-fill i a u ts = comp j a u (ts `conj` (i,j))
+fill i a u ts =
+  comp j (a `conj` (i,j)) u (insertSystem (i ~> 0) u (ts `conj` (i,j)))
   where j = fresh (Atom i,a,u,ts)
-fillNeg i a u ts = (fill i a u (ts `sym` i)) `sym` i
+fillNeg i a u ts = (fill i (a `sym` i) u (ts `sym` i)) `sym` i
 
-genFill, genFillNeg :: Name -> Val -> Val -> System Val -> Val
-genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j))
-  where j = fresh (Atom i,a,u,ts)
-genFillNeg i a u ts = (genFill i (a `sym` i) u (ts `sym` i)) `sym` i
+-- genFill, genFillNeg :: Name -> Val -> Val -> System Val -> Val
+-- genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j))
+--   where j = fresh (Atom i,a,u,ts)
+-- genFillNeg i a u ts = (genFill i (a `sym` i) u (ts `sym` i)) `sym` i
 
 comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
 comps i []         _ []         = []
 comps i ((x,a):as) e ((ts,u):tsus) =
-  let v   = genFill i (eval e a) u ts
-      vi1 = genComp i (eval e a) u ts
+  let v   = fill i (eval e a) u ts
+      vi1 = comp i (eval e a) u ts
       vs  = comps i as (upd (x,v) e) tsus
   in vi1 : vs
 comps _ _ _ _ = error "comps: different lengths of types and values"
 
--- i is independent of a and u
 comp :: Name -> Val -> Val -> System Val -> Val
 comp i a u ts | eps `Map.member` ts    = (ts ! eps) `face` (i ~> 1)
-comp i a u ts | i `notElem` support ts = u
-comp i a u ts | not (Map.null indep)   = comp i a u ts'
-  where (ts',indep) = Map.partition (\t -> i `elem` support t) ts
 comp i a u ts = case a of
-  VIdP p _ _ -> let j = fresh (Atom i,a,u,ts)
-                in VPath j $ comp i (p @@ j) (u @@ j) (Map.map (@@ j) ts)
+  VIdP p v0 v1 -> let j = fresh (Atom i,a,u,ts)
+                  in VPath j $ comp i (p @@ j) (u @@ j) $
+                       insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts)
   VSigma a f -> VPair ui1 comp_u2
     where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts)
           (u1,  u2)  = (fstVal u, sndVal u)
           fill_u1    = fill i a u1 t1s
           ui1        = comp i a u1 t1s
-          comp_u2    = genComp i (app f fill_u1) u2 t2s
-  VPi{} -> VComp a u (Map.map (VPath i) ts)
-  VU -> VComp VU u (Map.map (VPath i) ts)
+          comp_u2    = comp i (app f fill_u1) u2 t2s
+  VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts)
+  VU -> undefined
+    -- VComp VU u (Map.map (VPath i) ts)
+    -- VGlue u (Map.map (eqToIso i) ts)
   _ | isNeutral w -> w
     where w = VComp a u (Map.map (VPath i) ts)
-  VComp VU a es -> compU i a es u ts
+  -- VComp VU a es -> compU i a es u ts
   VGlue b hisos -> compGlue i b hisos u ts
-  VGlueLine b phi psi -> compGlueLine i b phi psi u ts
+  -- VGlueLine b phi psi -> compGlueLine i b phi psi u ts
   Ter (Sum _ _ nass) env -> case u of
     VCon n us -> case lookupLabel n nass of
       Just as ->
         if all isCon (elems ts)
            then let tsus = transposeSystemAndList (Map.map unCon ts) us
                 in VCon n $ comps i as env tsus
-           else VComp a u (Map.map (VPath i) ts)
+           else VComp (VPath i a) u (Map.map (VPath i) ts)
       Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
-    VPCon{} -> VComp a u (Map.map (VPath i) ts)
-    VComp{} -> VComp a u (Map.map (VPath i) ts)
-    VCompElem _ _ u1 _  -> comp i a u1 ts
-    VElimComp _ _ u1    -> comp i a u1 ts
+    VPCon{} -> compHIT i a u ts
+    VComp{} -> VComp (VPath i a) u (Map.map (VPath i) ts)
+    -- VCompElem _ _ u1 _  -> comp i a u1 ts
+    -- VElimComp _ _ u1    -> comp i a u1 ts
     _ -> error $ "comp ter sum" ++ show u
 
 compNeg :: Name -> Val -> Val -> System Val -> Val
-compNeg i a u ts = comp i a u (ts `sym` i)
+compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i)
 
 -- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
 -- fills i []         _ []         = []
 -- fills i ((x,a):as) e ((ts,u):tsus) =
---   let v  = genFill i (eval e a) ts u
+--   let v  = fill i (eval e a) ts u
 --       vs = fills i as (Upd e (x,v)) tsus
 --   in v : vs
 -- fills _ _ _ _ = error "fills: different lengths of types and values"
 
+-------------------------------------------------------------------------------
+-- | HIT
+
+compHIT :: Name -> Val -> Val -> System Val -> Val
+compHIT = undefined
+
+transpHIT :: Name -> Val -> Val -> Val
+transpHIT = undefined
+
+squeezeHIT :: Name -> Val -> Val -> Val
+squeezeHIT = undefined
+
 -------------------------------------------------------------------------------
 -- | Glue
 --
@@ -466,6 +494,11 @@ hisoFun :: Val -> Val
 hisoFun (VPair _ (VPair f _)) = f
 hisoFun x                     = error $ "HisoFun: Not an hiso: " ++ show x
 
+-- 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)
+
 glue :: Val -> System Val -> Val
 glue b ts | Map.null ts         = b
           | eps `Map.member` ts = hisoDom (ts ! eps)
@@ -482,8 +515,8 @@ unGlue hisos w
     | eps `Map.member` hisos = app (hisoFun (hisos ! eps)) w
     | otherwise              = case w of
        VGlueElem v us   -> v
-       VElimComp _ _ v -> unGlue hisos v
-       VCompElem a es v vs -> unGlue hisos v
+       -- VElimComp _ _ v -> unGlue hisos v
+       -- VCompElem a es v vs -> unGlue hisos v
        _ -> error $ "unGlue: " ++ show w ++ " should be neutral!"
 
 transGlue :: Name -> Val -> System Val -> Val -> Val
@@ -557,18 +590,20 @@ pathComp i a u u' us = VPath j $ comp i a (u `face` (i ~> 0)) us'
         us' = insertsSystem [(j ~> 0, u), (j ~> 1, u')] us
 
 
--- Grad Lemma, takes a iso an L-system ts a value v s.t. sigma us = border v
--- outputs u s.t. border u = us and an L-path between v and sigma u
--- an theta is a L path if L-border theta is constant
+-- Grad Lemma, takes an iso f, 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.
 gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
 gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v =
   (u, VPath i theta'')
-  where i:j:_   = freshs (a,hiso,us,v)
+  where i:j:_   = freshs (hiso,us,v)
         us'     = mapWithKey (\alpha uAlpha ->
                                    app (t `face` alpha) uAlpha @@ i) us
-        theta   = fill i a (app g v) us'
-        u       = comp i a (app g v) us'
-        ws      = insertSystem (i ~> 1) (app t u @@ j) $
+        gv      = app g v
+        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) (app t u @@ j) $
                   mapWithKey
                     (\alpha uAlpha ->
                       app (t `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us
@@ -585,229 +620,229 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v =
 -- | GlueLine
 
 
-glueLine :: Val -> Formula -> Formula -> Val
-glueLine t _ (Dir Zero)  = t
-glueLine t (Dir _) _     = t
-glueLine t phi (Dir One) = glue t isos
-  where isos = mkSystem (map (\alpha -> (alpha,idIso (t `face` alpha)))
-                         (invFormula phi Zero))
-glueLine t phi psi       = VGlueLine t phi psi
-
-idIso :: Val -> Val
-idIso a = VPair a $ VPair idV $ VPair idV $ VPair refl refl
-  where idV  = Ter (Lam "x" (Var "A") (Var "x")) (upd ("A",a) empty)
-        refl = Ter (Lam "x" (Var "A") (Path (Name "i") (Var "x")))
-                   (upd ("A",a) empty)
-
-glueLineElem :: Val -> Formula -> Formula -> Val
-glueLineElem u (Dir _) _     = u
-glueLineElem u _ (Dir Zero)  = u
-glueLineElem u phi (Dir One) = glueElem u ss
- where ss = mkSystem (map (\alpha -> (alpha,u `face` alpha))
-                      (invFormula phi Zero))
-glueLineElem u phi psi       = VGlueLineElem u phi psi
-
-unGlueLine :: Val -> Formula -> Formula -> Val -> Val
-unGlueLine b phi psi u = case (phi,psi,u) of
-   (Dir _,_,_)    -> u
-   (_,Dir Zero,_) -> u
-   (_,Dir One,_)  ->
-      let isos = mkSystem (map (\alpha -> (alpha,idIso (b `face` alpha)))
-                            (invFormula phi Zero))
-      in unGlue isos u
-   (_,_,VGlueLineElem w _ _ ) -> w
-   (_,_,_) -> error ("UnGlueLine, should be VGlueLineElem " ++ show u)
-
-compGlueLine :: Name -> Val -> Formula -> Formula -> Val -> System Val -> Val
-compGlueLine i b phi psi u us = glueLineElem vm phi psi
-  where fs = invFormula psi One
-        ws = mapWithKey
-               (\alpha -> unGlueLine (b `face` alpha)
-                            (phi `face` alpha) (psi `face` alpha)) us
-        w  = unGlueLine b phi psi u
-        v  = comp i b w ws
-
-        lss = mkSystem $ map
-                (\alpha ->
-                  (alpha,(phi `face` alpha,b `face` alpha,
-                          us `face` alpha,u `face` alpha))) fs
-        ls = mapWithKey (\alpha vAlpha ->
-                          auxGlueLine i vAlpha (v `face` alpha)) lss
-
-        vm = compLine b v ls
-
-auxGlueLine :: Name -> (Formula,Val,System Val,Val) -> Val -> Val
-auxGlueLine i (Dir _,b,ws,wi0) vi1 = VPath j vi1 where j = fresh vi1
-auxGlueLine i (phi,b,ws,wi0) vi1   = fillLine b vi1 ls'
-  where hisos = mkSystem (map (\alpha ->
-                  (alpha,idIso (b `face` alpha))) (invFormula phi Zero))
-        vs  = mapWithKey (\alpha -> unGlue (hisos `face` alpha)) ws
-        vi0 = unGlue hisos wi0 -- in b
-
-        v   = fill i b vi0 vs  -- in b
-        us' = mapWithKey (\gamma _ ->
-                           fill i (b `face` gamma) (wi0 `face` gamma)
-                             (ws `face` gamma))
-                hisos
-
-        ls' = mapWithKey (\gamma _ ->
-                           pathComp i (b `face` gamma) (v `face` gamma)
-                             (us' ! gamma) (vs `face` gamma))
-                hisos
-
-transGlueLine :: Name -> Val -> Formula -> Formula -> Val -> Val
-transGlueLine i b phi psi u = glueLineElem vm phii1 psii1
-  where fs = filter (i `Map.notMember`) (invFormula psi One)
-        phii1   = phi `face` (i ~> 1)
-        psii1   = psi `face` (i ~> 1)
-        phii0   = phi `face` (i ~> 0)
-        psii0   = psi `face` (i ~> 0)
-        bi1 = b `face`  (i ~> 1)
-        bi0 = b `face`  (i ~> 0)
-        lss = mkSystem (map (\ alpha ->
-                (alpha,(face phi alpha,face b alpha,face u alpha))) fs)
-        ls = mapWithKey (\alpha vAlpha ->
-               auxTransGlueLine i vAlpha (v `face` alpha)) lss
-        v = trans i b w
-        w  = unGlueLine bi0 phii0 psii0 u
-        vm = compLine bi1 v ls
-
-auxTransGlueLine :: Name -> (Formula,Val,Val) -> Val -> Val
-auxTransGlueLine i (Dir _,b,wi0) vi1 = VPath j vi1 where j = fresh vi1
-auxTransGlueLine i (phi,b,wi0) vi1   = fillLine (b `face` (i ~> 1)) vi1 ls'
-  where hisos = mkSystem (map (\ alpha ->
-                  (alpha,idIso (b `face` alpha))) (invFormula phi Zero))
-        vi0  = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0)
-        v    = transFill i b vi0           -- in b
-
-        -- set of elements in hisos independent of i
-        hisos'  = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos
-
-        us' = mapWithKey (\gamma _ ->
-                  transFill i (b `face` gamma) (wi0 `face` gamma))
-                hisos'
-
-        ls' = mapWithKey (\gamma _ ->
-                  VPath i $ squeeze i (b `face` gamma) (us' ! gamma))
-                hisos'
+-- glueLine :: Val -> Formula -> Formula -> Val
+-- glueLine t _ (Dir Zero)  = t
+-- glueLine t (Dir _) _     = t
+-- glueLine t phi (Dir One) = glue t isos
+--   where isos = mkSystem (map (\alpha -> (alpha,idIso (t `face` alpha)))
+--                          (invFormula phi Zero))
+-- glueLine t phi psi       = VGlueLine t phi psi
+
+-- idIso :: Val -> Val
+-- idIso a = VPair a $ VPair idV $ VPair idV $ VPair refl refl
+--   where idV  = Ter (Lam "x" (Var "A") (Var "x")) (upd ("A",a) empty)
+--         refl = Ter (Lam "x" (Var "A") (Path (Name "i") (Var "x")))
+--                    (upd ("A",a) empty)
+
+-- glueLineElem :: Val -> Formula -> Formula -> Val
+-- glueLineElem u (Dir _) _     = u
+-- glueLineElem u _ (Dir Zero)  = u
+-- glueLineElem u phi (Dir One) = glueElem u ss
+--  where ss = mkSystem (map (\alpha -> (alpha,u `face` alpha))
+--                       (invFormula phi Zero))
+-- glueLineElem u phi psi       = VGlueLineElem u phi psi
+
+-- unGlueLine :: Val -> Formula -> Formula -> Val -> Val
+-- unGlueLine b phi psi u = case (phi,psi,u) of
+--    (Dir _,_,_)    -> u
+--    (_,Dir Zero,_) -> u
+--    (_,Dir One,_)  ->
+--       let isos = mkSystem (map (\alpha -> (alpha,idIso (b `face` alpha)))
+--                             (invFormula phi Zero))
+--       in unGlue isos u
+--    (_,_,VGlueLineElem w _ _ ) -> w
+--    (_,_,_) -> error ("UnGlueLine, should be VGlueLineElem " ++ show u)
+
+-- compGlueLine :: Name -> Val -> Formula -> Formula -> Val -> System Val -> Val
+-- compGlueLine i b phi psi u us = glueLineElem vm phi psi
+--   where fs = invFormula psi One
+--         ws = mapWithKey
+--                (\alpha -> unGlueLine (b `face` alpha)
+--                             (phi `face` alpha) (psi `face` alpha)) us
+--         w  = unGlueLine b phi psi u
+--         v  = comp i b w ws
+
+--         lss = mkSystem $ map
+--                 (\alpha ->
+--                   (alpha,(phi `face` alpha,b `face` alpha,
+--                           us `face` alpha,u `face` alpha))) fs
+--         ls = mapWithKey (\alpha vAlpha ->
+--                           auxGlueLine i vAlpha (v `face` alpha)) lss
+
+--         vm = compLine b v ls
+
+-- auxGlueLine :: Name -> (Formula,Val,System Val,Val) -> Val -> Val
+-- auxGlueLine i (Dir _,b,ws,wi0) vi1 = VPath j vi1 where j = fresh vi1
+-- auxGlueLine i (phi,b,ws,wi0) vi1   = fillLine b vi1 ls'
+--   where hisos = mkSystem (map (\alpha ->
+--                   (alpha,idIso (b `face` alpha))) (invFormula phi Zero))
+--         vs  = mapWithKey (\alpha -> unGlue (hisos `face` alpha)) ws
+--         vi0 = unGlue hisos wi0 -- in b
+
+--         v   = fill i b vi0 vs  -- in b
+--         us' = mapWithKey (\gamma _ ->
+--                            fill i (b `face` gamma) (wi0 `face` gamma)
+--                              (ws `face` gamma))
+--                 hisos
+
+--         ls' = mapWithKey (\gamma _ ->
+--                            pathComp i (b `face` gamma) (v `face` gamma)
+--                              (us' ! gamma) (vs `face` gamma))
+--                 hisos
+
+-- transGlueLine :: Name -> Val -> Formula -> Formula -> Val -> Val
+-- transGlueLine i b phi psi u = glueLineElem vm phii1 psii1
+--   where fs = filter (i `Map.notMember`) (invFormula psi One)
+--         phii1   = phi `face` (i ~> 1)
+--         psii1   = psi `face` (i ~> 1)
+--         phii0   = phi `face` (i ~> 0)
+--         psii0   = psi `face` (i ~> 0)
+--         bi1 = b `face`  (i ~> 1)
+--         bi0 = b `face`  (i ~> 0)
+--         lss = mkSystem (map (\ alpha ->
+--                 (alpha,(face phi alpha,face b alpha,face u alpha))) fs)
+--         ls = mapWithKey (\alpha vAlpha ->
+--                auxTransGlueLine i vAlpha (v `face` alpha)) lss
+--         v = trans i b w
+--         w  = unGlueLine bi0 phii0 psii0 u
+--         vm = compLine bi1 v ls
+
+-- auxTransGlueLine :: Name -> (Formula,Val,Val) -> Val -> Val
+-- auxTransGlueLine i (Dir _,b,wi0) vi1 = VPath j vi1 where j = fresh vi1
+-- auxTransGlueLine i (phi,b,wi0) vi1   = fillLine (b `face` (i ~> 1)) vi1 ls'
+--   where hisos = mkSystem (map (\ alpha ->
+--                   (alpha,idIso (b `face` alpha))) (invFormula phi Zero))
+--         vi0  = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0)
+--         v    = transFill i b vi0           -- in b
+
+--         -- set of elements in hisos independent of i
+--         hisos'  = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos
+
+--         us' = mapWithKey (\gamma _ ->
+--                   transFill i (b `face` gamma) (wi0 `face` gamma))
+--                 hisos'
+
+--         ls' = mapWithKey (\gamma _ ->
+--                   VPath i $ squeeze i (b `face` gamma) (us' ! gamma))
+--                 hisos'
 
 
 
 -------------------------------------------------------------------------------
 -- | Composition in the Universe
 
-isConstPath :: Val -> Bool
-isConstPath (VPath i u) = i `notElem` support u
-isConstPath _ = False
-
-compElem :: Val -> System Val -> Val -> System Val -> Val
-compElem a es u us = compElem' (Map.filter (not . isConstPath) es)
-  where compElem' es | Map.null es         = u
-                     | eps `Map.member` us = us ! eps
-                     | otherwise           = VCompElem a es u us
-
-elimComp :: Val -> System Val -> Val -> Val
-elimComp a es u = elimComp' (Map.filter (not . isConstPath) es)
-  where elimComp' es | Map.null es         = u
-                     | eps `Map.member` es = transNegLine (es ! eps) u
-                     | otherwise           = VElimComp a es u
-
-compU :: Name -> Val -> System Val -> Val -> System Val -> Val
-compU i a es w0 ws =
-    let vs = mapWithKey
-               (\alpha -> elimComp (a `face` alpha) (es `face` alpha)) ws
-        v0 = elimComp a es w0 -- in a
-        v1 = comp i a v0 vs -- in a
-
-        us1' = mapWithKey (\gamma eGamma ->
-                            comp i (eGamma @@ One) (w0 `face` gamma)
-                                   (ws `face` gamma)) es
-        ls' = mapWithKey
-                (\gamma eGamma -> pathUniv i eGamma
-                                  (ws `face` gamma) (w0 `face` gamma))
-                es
-
-        v1' = compLine a v1 ls'
-    in compElem a es v1' us1'
-
--- Computes a homotopy between the image of the composition, and the
--- composition of the image. Given e (an equality in U), an L-system
--- us (in e0) and ui0 (in e0 (i0)) The output is an L(i1)-path in
--- e1(i1) between vi1 and sigma (i1) ui1 where
---   sigma = appEq
---   ui1 = comp i (e 0) us ui0
---   vi1 = comp i (e 1) (sigma us) (sigma(i0) ui0)
--- Moreover, if e is constant, so is the output.
-pathUniv :: Name -> Val -> System Val -> Val -> Val
-pathUniv i e us ui0 = VPath k xi1
-  where j:k:_ = freshs (Atom i,e,us,ui0)
-        ej    = e @@ j
-        ui1   = comp i (e @@ One) ui0 us
-        ws    = mapWithKey (\alpha uAlpha ->
-                  transFillNeg j (ej `face` alpha) uAlpha)
-                us
-        wi0   = transFillNeg j (ej `face` (i ~> 0)) ui0
-        wi1   = comp i ej wi0 ws
-        wi1'  = transFillNeg j (ej `face` (i ~> 1)) ui1
-        xi1   = genCompNeg j (ej `face` (i ~> 1)) ui1
-                  (mkSystem [(k ~> 1, wi1'), (k ~> 0, wi1)])
-
-transU :: Name -> Val -> System Val -> Val -> Val
-transU i a es wi0 =
-  let vi0 = elimComp (a `face` (i ~> 0)) (es `face` (i ~> 0)) wi0 -- in a(i0)
-      vi1 = trans i a vi0      -- in a(i1)
-
-      ai1  = a `face` (i ~> 1)
-      esi1 = es `face` (i ~> 1)
-
-      -- gamma in es'' iff i not in the domain of gamma and (i1)gamma in es
-      es'' = filterWithKey (\alpha _ -> alpha `Map.notMember` es) esi1
-
-      -- set of faces alpha of es such i is not the domain of alpha
-      es'  = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es
-
-      usi1' = mapWithKey (\gamma eGamma ->
-                trans i (eGamma @@ One) (wi0 `face` gamma)) es'
-
-      ls' = mapWithKey (\gamma _ ->
-              pathUnivTrans i (es `proj` gamma) (wi0 `face` gamma))
---                         pathUniv i (es `proj` gamma) Map.empty (wi0 `face` gamma))
-            es'
-
-      vi1' = compLine ai1 vi1 ls'
-
-      uls'' = mapWithKey (\gamma _ -> -- Should be !, not proj ?
-                eqLemma (es ! (gamma `meet` (i ~> 1)))
-                        (usi1' `face` gamma) (vi1' `face` gamma)) es''
-
-      vi1'' = compLine ai1 vi1' (Map.map snd uls'')
-
-      usi1  = mapWithKey (\gamma _ ->
-                if gamma `Map.member` usi1' then usi1' ! gamma
-                else fst (uls'' ! gamma)) esi1
-  in compElem ai1 esi1 vi1'' usi1
-
-
-pathUnivTrans :: Name -> Val -> Val -> Val
-pathUnivTrans i e ui0 = VPath j xi1
-  where j    = fresh (Atom i,e,ui0)
-        ej   = e @@ j
-        wi0  = transFillNeg j (ej `face` (i ~> 0)) ui0
-        wi1  = trans i ej wi0
-        xi1  = squeezeNeg j (ej `face` (i ~> 1)) wi1
-
--- Any equality defines an equivalence.
-eqLemma :: Val -> System Val -> Val -> (Val, Val)
-eqLemma e ts a = (t,VPath j theta'')
-  where i:j:_   = freshs (e,ts,a)
-        ei      = e @@ i
-        vs      = mapWithKey (\alpha uAlpha ->
-                    transFillNeg i (ei `face` alpha) uAlpha) ts
-        theta   = genFill i ei a vs
-        t       = genComp i ei a vs
-        theta'  = transFillNeg i ei t
-        ws      = insertSystem (j ~> 1) theta' $ insertSystem (j ~> 0) theta vs
-        theta'' = genCompNeg i ei t ws
+-- isConstPath :: Val -> Bool
+-- isConstPath (VPath i u) = i `notElem` support u
+-- isConstPath _ = False
+
+-- compElem :: Val -> System Val -> Val -> System Val -> Val
+-- compElem a es u us = compElem' (Map.filter (not . isConstPath) es)
+--   where compElem' es | Map.null es         = u
+--                      | eps `Map.member` us = us ! eps
+--                      | otherwise           = VCompElem a es u us
+
+-- elimComp :: Val -> System Val -> Val -> Val
+-- elimComp a es u = elimComp' (Map.filter (not . isConstPath) es)
+--   where elimComp' es | Map.null es         = u
+--                      | eps `Map.member` es = transNegLine (es ! eps) u
+--                      | otherwise           = VElimComp a es u
+
+-- compU :: Name -> Val -> System Val -> Val -> System Val -> Val
+-- compU i a es w0 ws =
+--     let vs = mapWithKey
+--                (\alpha -> elimComp (a `face` alpha) (es `face` alpha)) ws
+--         v0 = elimComp a es w0 -- in a
+--         v1 = comp i a v0 vs -- in a
+
+--         us1' = mapWithKey (\gamma eGamma ->
+--                             comp i (eGamma @@ One) (w0 `face` gamma)
+--                                    (ws `face` gamma)) es
+--         ls' = mapWithKey
+--                 (\gamma eGamma -> pathUniv i eGamma
+--                                   (ws `face` gamma) (w0 `face` gamma))
+--                 es
+
+--         v1' = compLine a v1 ls'
+--     in compElem a es v1' us1'
+
+-- -- Computes a homotopy between the image of the composition, and the
+-- -- composition of the image. Given e (an equality in U), an L-system
+-- -- us (in e0) and ui0 (in e0 (i0)) The output is an L(i1)-path in
+-- -- e1(i1) between vi1 and sigma (i1) ui1 where
+-- --   sigma = appEq
+-- --   ui1 = comp i (e 0) us ui0
+-- --   vi1 = comp i (e 1) (sigma us) (sigma(i0) ui0)
+-- -- Moreover, if e is constant, so is the output.
+-- pathUniv :: Name -> Val -> System Val -> Val -> Val
+-- pathUniv i e us ui0 = VPath k xi1
+--   where j:k:_ = freshs (Atom i,e,us,ui0)
+--         ej    = e @@ j
+--         ui1   = comp i (e @@ One) ui0 us
+--         ws    = mapWithKey (\alpha uAlpha ->
+--                   transFillNeg j (ej `face` alpha) uAlpha)
+--                 us
+--         wi0   = transFillNeg j (ej `face` (i ~> 0)) ui0
+--         wi1   = comp i ej wi0 ws
+--         wi1'  = transFillNeg j (ej `face` (i ~> 1)) ui1
+--         xi1   = compNeg j (ej `face` (i ~> 1)) ui1
+--                   (mkSystem [(k ~> 1, wi1'), (k ~> 0, wi1)])
+
+-- transU :: Name -> Val -> System Val -> Val -> Val
+-- transU i a es wi0 =
+--   let vi0 = elimComp (a `face` (i ~> 0)) (es `face` (i ~> 0)) wi0 -- in a(i0)
+--       vi1 = trans i a vi0      -- in a(i1)
+
+--       ai1  = a `face` (i ~> 1)
+--       esi1 = es `face` (i ~> 1)
+
+--       -- gamma in es'' iff i not in the domain of gamma and (i1)gamma in es
+--       es'' = filterWithKey (\alpha _ -> alpha `Map.notMember` es) esi1
+
+--       -- set of faces alpha of es such i is not the domain of alpha
+--       es'  = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es
+
+--       usi1' = mapWithKey (\gamma eGamma ->
+--                 trans i (eGamma @@ One) (wi0 `face` gamma)) es'
+
+--       ls' = mapWithKey (\gamma _ ->
+--               pathUnivTrans i (es `proj` gamma) (wi0 `face` gamma))
+-- --                         pathUniv i (es `proj` gamma) Map.empty (wi0 `face` gamma))
+--             es'
+
+--       vi1' = compLine ai1 vi1 ls'
+
+--       uls'' = mapWithKey (\gamma _ -> -- Should be !, not proj ?
+--                 eqLemma (es ! (gamma `meet` (i ~> 1)))
+--                         (usi1' `face` gamma) (vi1' `face` gamma)) es''
+
+--       vi1'' = compLine ai1 vi1' (Map.map snd uls'')
+
+--       usi1  = mapWithKey (\gamma _ ->
+--                 if gamma `Map.member` usi1' then usi1' ! gamma
+--                 else fst (uls'' ! gamma)) esi1
+--   in compElem ai1 esi1 vi1'' usi1
+
+
+-- pathUnivTrans :: Name -> Val -> Val -> Val
+-- pathUnivTrans i e ui0 = VPath j xi1
+--   where j    = fresh (Atom i,e,ui0)
+--         ej   = e @@ j
+--         wi0  = transFillNeg j (ej `face` (i ~> 0)) ui0
+--         wi1  = trans i ej wi0
+--         xi1  = squeezeNeg j (ej `face` (i ~> 1)) wi1
+
+-- -- Any equality defines an equivalence.
+-- eqLemma :: Val -> System Val -> Val -> (Val, Val)
+-- eqLemma e ts a = (t,VPath j theta'')
+--   where i:j:_   = freshs (e,ts,a)
+--         ei      = e @@ i
+--         vs      = mapWithKey (\alpha uAlpha ->
+--                     transFillNeg i (ei `face` alpha) uAlpha) ts
+--         theta   = fill i ei a vs
+--         t       = comp i ei a vs
+--         theta'  = transFillNeg i ei t
+--         ws      = insertSystem (j ~> 1) theta' $ insertSystem (j ~> 0) theta vs
+--         theta'' = compNeg i ei t ws
 
 
 -------------------------------------------------------------------------------
@@ -816,37 +851,37 @@ eqLemma e ts a = (t,VPath j theta'')
 class Convertible a where
   conv :: [String] -> a -> a -> Bool
 
-isIndep :: (Nominal a, Convertible a) => [String] -> Name -> a -> Bool
-isIndep ns i u = conv ns u (u `face` (i ~> 0))
+-- isIndep :: (Nominal a, Convertible a) => [String] -> Name -> a -> Bool
+-- isIndep ns i u = conv ns u (u `face` (i ~> 0))
 
 isCompSystem :: (Nominal a, Convertible a) => [String] -> System a -> Bool
 isCompSystem ns ts = and [ conv ns (getFace alpha beta) (getFace beta alpha)
                          | (alpha,beta) <- allCompatible (keys ts) ]
     where getFace a b = face (ts ! a) (b `minus` a)
 
-simplify :: [String] -> Name -> Val -> Val
-simplify ns j v = case v of
-  VTrans p u | isIndep ns j (p @@ j) -> simplify ns j u
-  VComp a u ts ->
-    let (indep,ts') = Map.partition (\t -> isIndep ns j (t @@ j)) ts
-    in if Map.null ts' then simplify ns j u else VComp a u ts'
-  VCompElem a es u us ->
-    let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es
-        us'         = intersection us es'
-    in if Map.null es' then simplify ns j u else VCompElem a es' u us'
-  VElimComp a es u ->
-    let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es
-        u'          = simplify ns j u
-    in if Map.null es' then u' else case u' of
-      VCompElem _ _ w _ -> simplify ns j w
-      _ -> VElimComp a es' u'
-  _ -> v
+-- simplify :: [String] -> Name -> Val -> Val
+-- simplify ns j v = case v of
+--   VTrans p u | isIndep ns j (p @@ j) -> simplify ns j u
+--   VComp a u ts ->
+--     let (indep,ts') = Map.partition (\t -> isIndep ns j (t @@ j)) ts
+--     in if Map.null ts' then simplify ns j u else VComp a u ts'
+--   VCompElem a es u us ->
+--     let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es
+--         us'         = intersection us es'
+--     in if Map.null es' then simplify ns j u else VCompElem a es' u us'
+--   VElimComp a es u ->
+--     let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es
+--         u'          = simplify ns j u
+--     in if Map.null es' then u' else case u' of
+--       VCompElem _ _ w _ -> simplify ns j w
+--       _ -> VElimComp a es' u'
+--   _ -> v
 
 instance Convertible Val where
   conv ns u v | u == v    = True
               | otherwise =
     let j = fresh (u,v)
-    in case (simplify ns j u, simplify ns j v) of
+    in case (u,v) of
       (Ter (Lam x a u) e,Ter (Lam x' a' u') e') ->
         let v@(VVar n _) = mkVarNice ns x (eval e a)
         in conv (n:ns) (eval (upd (x,v) e) u) (eval (upd (x',v) e') u')
@@ -883,14 +918,14 @@ instance Convertible Val where
       (VPath i a,VPath i' a')    -> conv ns (a `swap` (i,j)) (a' `swap` (i',j))
       (VPath i a,p')             -> conv ns (a `swap` (i,j)) (p' @@ j)
       (p,VPath i' a')            -> conv ns (p @@ j) (a' `swap` (i',j))
-      (VTrans p u,VTrans p' u')  -> conv ns p p' && conv ns u u'
+      -- (VTrans p u,VTrans p' u')  -> conv ns p p' && conv ns u u'
       (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x')
       (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts')
       (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos')
       (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us')
-      (VCompElem a es u us,VCompElem a' es' u' us') ->
-        conv ns (a,es,u,us) (a',es',u',us')
-      (VElimComp a es u,VElimComp a' es' u') -> conv ns (a,es,u) (a',es',u')
+      -- (VCompElem a es u us,VCompElem a' es' u' us') ->
+      --   conv ns (a,es,u,us) (a',es',u',us')
+      -- (VElimComp a es u,VElimComp a' es' u') -> conv ns (a,es,u) (a',es',u')
       _                         -> False
 
 instance Convertible Ctxt where
@@ -943,11 +978,11 @@ instance Normal Val where
     VIdP a u0 u1        -> VIdP (normal ns a) (normal ns u0) (normal ns u1)
     VPath i u           -> VPath i (normal ns u)
     VComp u v vs        -> compLine (normal ns u) (normal ns v) (normal ns vs)
-    VTrans u v          -> transLine (normal ns u) (normal ns v)
+    -- VTrans u v          -> transLine (normal ns u) (normal ns v)
     VGlue u hisos       -> glue (normal ns u) (normal ns hisos)
     VGlueElem u us      -> glueElem (normal ns u) (normal ns us)
-    VCompElem a es u us -> compElem (normal ns a) (normal ns es) (normal ns u) (normal ns us)
-    VElimComp a es u    -> elimComp (normal ns a) (normal ns es) (normal ns u)
+    -- VCompElem a es u us -> compElem (normal ns a) (normal ns es) (normal ns u) (normal ns us)
+    -- VElimComp a es u    -> elimComp (normal ns a) (normal ns es) (normal ns u)
     VVar x t            -> VVar x t -- (normal ns t)
     VFst t              -> fstVal (normal ns t)
     VSnd t              -> sndVal (normal ns t)