Reintroduce compU

diff --git a/CTT.hs b/CTT.hs
index 114b316af7897df25d5de39363238c8702308724..5166b33c109b723acc0d3d19fc2edc7276caef80 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -146,6 +146,9 @@ 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)
 
@@ -157,6 +160,9 @@ data Val = VU
          | VApp Val Val
          | VAppFormula Val Formula
          | VLam Ident Val Val
+
+         | VUnGlueElemU Val Val (System Val)
+
   deriving Eq
 
 isNeutral :: Val -> Bool
@@ -170,6 +176,7 @@ isNeutral v = case v of
   VSplit{}       -> True
   VApp{}         -> True
   VAppFormula{}  -> True
+  VUnGlueElemU{} -> True
   _              -> False
 
 isNeutralSystem :: System Val -> Bool
@@ -387,6 +394,9 @@ showVal v = case v of
     text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
   VGlue a ts        -> text "glue" <+> showVal1 a <+> text (showSystem ts)
   VGlueElem a ts    -> text "glueElem" <+> showVal1 a <+> text (showSystem ts)
+  VUnGlueElemU v b es -> text "unGlueElemU" <+> showVals [v,b]
+                         <+> text (showSystem es)
+  VCompU a ts       -> text "compU" <+> showVal1 a <+> text (showSystem ts)
 
 showPath :: Val -> Doc
 showPath e = case e of

diff --git a/Eval.hs b/Eval.hs
index 4e7a911391e8a3886ad0fdc83443a458f779f80a..63e816a879a72341f1ff21da38548dbd1c981002 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -71,6 +71,8 @@ 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)
+    VUnGlueElemU a b es     -> support (a,b,es)
 
   act u (i, phi) | i `notElem` support u = u
                  | otherwise =
@@ -101,6 +103,8 @@ 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)
+         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,6 +131,8 @@ 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)
+         VUnGlueElemU a b es     -> VUnGlueElemU (sw a) (sw b) (sw es)
+         VCompU a ts             -> VCompU (sw a) (sw ts)
 
 
 -----------------------------------------------------------------------
@@ -261,6 +267,8 @@ v @@ phi                   = error $ "(@@): " ++ show v ++ " should be neutral."
 -------------------------------------------------------------------------------
 -- Composition and filling
 
+
+
 comp :: Name -> Val -> Val -> System Val -> Val
 comp i a u ts | eps `member` ts = (ts ! eps) `face` (i ~> 1)
 comp i a u ts = case a of
@@ -274,7 +282,8 @@ 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    -> glue u (Map.map (eqToIso . VPath i) ts)
+  VU -> compUniv u (Map.map (VPath i) ts)
+  -- VU    -> glue u (Map.map (eqToIso . VPath i) ts)
   VGlue b isos | not (isNeutralGlue i isos u ts) -> compGlue i b isos u ts
   Ter (Sum _ _ nass) env -> case u of
     VCon n us | all isCon (elems ts) -> case lookupLabel n nass of
@@ -590,6 +599,113 @@ gradLemma b iso us v = (u, VPath i theta'')
                       app (s `face` alpha) (app (f `face` alpha) uAlpha) @@ j) us
         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
 

diff --git a/examples/shortsetquot.ctt b/examples/shortsetquot.ctt
index 2be6de5f1b17b268fe50474361c1e7aebb9da14d..3c3b50df9f288171c3c3806dbd4d783aee4c74d5 100644 (file)
--- a/examples/shortsetquot.ctt
+++ b/examples/shortsetquot.ctt
@@ -180,6 +180,13 @@ K' (t : setquot bool R.1) : (P' t).1 = setquotunivprop bool R P' ps t
 test : (P' true').1 = hdisj_in1 (Id (setquot bool R.1) true' true')
                                 (Id (setquot bool R.1) true' false') (<_> true')
 
+test' : (P' true').1 = K' true'
+
+test'' : Id (P' true').1 test test' = (P' true').2 test test'
+
+-- test' : Id (P' true').1 (K' true')
+--           (hdisj_in1 (Id (setquot bool R.1) true' true') (Id (setquot bool R.1) true' false') (<_> true')) =
+--   <_> K' true'
 
 -- This takes too long:
 -- > :n K' true'