rename Eq to Id

diff --git a/CTT.hs b/CTT.hs
index f974c4b6d6d65822249ffe371a394f4a764405f9..de3c8c7c3e9253a5e59c881b3eab1f674122ad9c 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -119,10 +119,10 @@ data Ter = Pi Ter
          | Glue Ter (System Ter)
          | GlueElem Ter (System Ter)
          | UnGlueElem Ter (System Ter)
-           -- Eq
-         | Eq Ter Ter Ter
-         | EqPair Ter (System Ter)
-         | EqJ Ter Ter Ter Ter Ter Ter
+           -- Id
+         | Id Ter Ter Ter
+         | IdPair Ter (System Ter)
+         | IdJ Ter Ter Ter Ter Ter Ter
   deriving Eq
 
 -- For an expression t, returns (u,ts) where u is no application and t = u ts
@@ -167,9 +167,9 @@ data Val = VU
            -- Composition for HITs; the type is constant
          | VHComp Val Val (System Val)
 
-           -- Eq
-         | VEq Val Val Val
-         | VEqPair Val (System Val)
+           -- Id
+         | VId Val Val Val
+         | VIdPair Val (System Val)
 
            -- Neutral values:
          | VVar Ident Val
@@ -181,7 +181,7 @@ data Val = VU
          | VAppFormula Val Formula
          | VLam Ident Val Val
          | VUnGlueElemU Val Val (System Val)
-         | VEqJ Val Val Val Val Val Val
+         | VIdJ Val Val Val Val Val Val
   deriving Eq
 
 isNeutral :: Val -> Bool
@@ -198,7 +198,7 @@ isNeutral v = case v of
   VAppFormula{}  -> True
   VUnGlueElemU{} -> True
   VUnGlueElem{}  -> True
-  VEqJ{}         -> True
+  VIdJ{}         -> True
   _              -> False
 
 isNeutralSystem :: System Val -> Bool
@@ -383,9 +383,9 @@ showTer v = case v of
   Glue a ts          -> text "Glue" <+> showTer1 a <+> text (showSystem ts)
   GlueElem a ts      -> text "glue" <+> showTer1 a <+> text (showSystem ts)
   UnGlueElem a ts    -> text "unglue" <+> showTer1 a <+> text (showSystem ts)
-  Eq a u v           -> text "Eq" <+> showTers [a,u,v]
-  EqPair b ts        -> text "eqC" <+> showTer1 b <+> text (showSystem ts)
-  EqJ a t c d x p    -> text "eqJ" <+> showTers [a,t,c,d,x,p]
+  Id a u v           -> text "Id" <+> showTers [a,u,v]
+  IdPair b ts        -> text "IdC" <+> showTer1 b <+> text (showSystem ts)
+  IdJ a t c d x p    -> text "IdJ" <+> showTers [a,t,c,d,x,p]
 
 showTers :: [Ter] -> Doc
 showTers = hsep . map showTer1

diff --git a/Eval.hs b/Eval.hs
index 3b60833c749c360f933f9404afb0af4ccc6568dd..268121414bfe52819c721c8d039c947b262f0313 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -77,9 +77,9 @@ instance Nominal Val where
     VUnGlueElem a ts        -> support (a,ts)
     VCompU a ts             -> support (a,ts)
     VUnGlueElemU a b es     -> support (a,b,es)
-    VEqPair u us            -> support (u,us)
-    VEq a u v               -> support (a,u,v)
-    VEqJ a u c d x p        -> support [a,u,c,d,x,p]
+    VIdPair u us            -> support (u,us)
+    VId a u v               -> support (a,u,v)
+    VIdJ a u c d x p        -> support [a,u,c,d,x,p]
 
   act u (i, phi) | i `notElem` support u = u
                  | otherwise =
@@ -114,10 +114,10 @@ instance Nominal Val where
          VUnGlueElem a ts        -> unglueElem (acti a) (acti ts)
          VUnGlueElemU a b es     -> unGlueU (acti a) (acti b) (acti es)
          VCompU a ts             -> compUniv (acti a) (acti ts)
-         VEqPair u us            -> VEqPair (acti u) (acti us)
-         VEq a u v               -> VEq (acti a) (acti u) (acti v)
-         VEqJ a u c d x p        ->
-           eqJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p)
+         VIdPair u us            -> VIdPair (acti u) (acti us)
+         VId a u v               -> VId (acti a) (acti u) (acti v)
+         VIdJ a u c d x p        ->
+           idJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p)
 
   -- This increases efficiency as it won't trigger computation.
   swap u ij@(i,j) =
@@ -148,10 +148,10 @@ instance Nominal Val where
          VUnGlueElem a ts        -> VUnGlueElem (sw a) (sw ts)
          VUnGlueElemU a b es     -> VUnGlueElemU (sw a) (sw b) (sw es)
          VCompU a ts             -> VCompU (sw a) (sw ts)
-         VEqPair u us            -> VEqPair (sw u) (sw us)
-         VEq a u v               -> VEq (sw a) (sw u) (sw v)
-         VEqJ a u c d x p        ->
-           VEqJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p)
+         VIdPair u us            -> VIdPair (sw u) (sw us)
+         VId a u v               -> VId (sw a) (sw u) (sw v)
+         VIdJ a u c d x p        ->
+           VIdJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p)
 
 -----------------------------------------------------------------------
 -- The evaluator
@@ -189,9 +189,9 @@ eval rho@(_,_,_,Nameless os) v = case v of
   Glue a ts           -> glue (eval rho a) (evalSystem rho ts)
   GlueElem a ts       -> glueElem (eval rho a) (evalSystem rho ts)
   UnGlueElem a ts     -> unglueElem (eval rho a) (evalSystem rho ts)
-  Eq a r s            -> VEq (eval rho a) (eval rho r) (eval rho s)
-  EqPair b ts         -> VEqPair (eval rho b) (evalSystem rho ts)
-  EqJ a t c d x p     -> eqJ (eval rho a) (eval rho t) (eval rho c)
+  Id a r s            -> VId (eval rho a) (eval rho r) (eval rho s)
+  IdPair b ts         -> VIdPair (eval rho b) (evalSystem rho ts)
+  IdJ a t c d x p     -> idJ (eval rho a) (eval rho t) (eval rho c)
                              (eval rho d) (eval rho x) (eval rho p)
   _                   -> error $ "Cannot evaluate " ++ show v
 
@@ -280,7 +280,7 @@ inferType v = case v of
   VComp a _ _ -> a @@ One
 --  VUnGlueElem _ b _  -> b   -- This is wrong! Store the type??
   VUnGlueElemU _ b _ -> b
-  VEqJ _ _ c _ x p -> app (app c x) p
+  VIdJ _ _ c _ x p -> app (app c x) p
   _ -> error $ "inferType: not neutral " ++ show v
 
 (@@) :: ToFormula a => Val -> a -> Val
@@ -307,15 +307,15 @@ comp i a u ts = case a of
   VPathP p v0 v1 -> let j = fresh (Atom i,a,u,ts)
                     in VPLam j $ comp i (p @@ j) (u @@ j) $
                          insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts)
-  VEq b v0 v1 -> case u of
-    VEqPair r _ | all isEqPair (elems ts) ->
+  VId b v0 v1 -> case u of
+    VIdPair r _ | all isIdPair (elems ts) ->
       let j = fresh (Atom i,a,u,ts)
-          VEqPair z _ @@@ phi = z @@ phi
-          sys (VEqPair _ ws)  = ws
+          VIdPair z _ @@@ phi = z @@ phi
+          sys (VIdPair _ ws)  = ws
           w = VPLam j $ comp i b (r @@ j) $
                           insertsSystem [(j ~> 0,v0),(j ~> 1,v1)]
                             (Map.map (@@@ j) ts)
-      in VEqPair w (joinSystem (Map.map sys (ts `face` (i ~> 1))))
+      in VIdPair w (joinSystem (Map.map sys (ts `face` (i ~> 1))))
     _ -> VComp (VPLam i a) u (Map.map (VPLam i) ts)
   VSigma a f -> VPair ui1 comp_u2
     where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts)
@@ -424,20 +424,20 @@ squeezes i xas e us = comps j xas (e `disj` (i,j)) us'
 
 
 -------------------------------------------------------------------------------
--- | Eq
+-- | Id
 
-eqJ :: Val -> Val -> Val -> Val -> Val -> Val -> Val
-eqJ a v c d x p = case p of
-  VEqPair w ws -> comp i (app (app c (w @@ i)) w') d
+idJ :: Val -> Val -> Val -> Val -> Val -> Val -> Val
+idJ a v c d x p = case p of
+  VIdPair w ws -> comp i (app (app c (w @@ i)) w') d
                     (border d (shape ws))
-    where w' = VEqPair (VPLam j $ w @@ (Atom i :/\: Atom j))
+    where w' = VIdPair (VPLam j $ w @@ (Atom i :/\: Atom j))
                   (insertSystem (i ~> 0) v ws)
           i:j:_ = freshs [a,v,c,d,x,p]
-  _ -> VEqJ a v c d x p
+  _ -> VIdJ a v c d x p
 
-isEqPair :: Val -> Bool
-isEqPair VEqPair{} = True
-isEqPair _         = False
+isIdPair :: Val -> Bool
+isIdPair VIdPair{} = True
+isIdPair _         = False
 
 
 -------------------------------------------------------------------------------
@@ -884,9 +884,9 @@ instance Convertible Val where
       (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'
       (VUnGlueElem u ts,VUnGlueElem u' ts')    -> conv ns (u,ts) (u',ts')
       (VCompU u es,VCompU u' es')              -> conv ns (u,es) (u',es')
-      (VEqPair v vs,VEqPair v' vs')          -> conv ns (v,vs) (v',vs')
-      (VEq a u v,VEq a' u' v')               -> conv ns (a,u,v) (a',u',v')
-      (VEqJ a u c d x p,VEqJ a' u' c' d' x' p') ->
+      (VIdPair v vs,VIdPair v' vs')          -> conv ns (v,vs) (v',vs')
+      (VId a u v,VId a' u' v')               -> conv ns (a,u,v) (a',u',v')
+      (VIdJ a u c d x p,VIdJ a' u' c' d' x' p') ->
         conv ns [a,u,c,d,x,p] [a',u',c',d',x',p']
       _                                      -> False
 
@@ -955,9 +955,9 @@ instance Normal Val where
     VSplit u t          -> VSplit (normal ns u) (normal ns t)
     VApp u v            -> app (normal ns u) (normal ns v)
     VAppFormula u phi   -> VAppFormula (normal ns u) (normal ns phi)
-    VEq a u v           -> VEq (normal ns a) (normal ns u) (normal ns v)
-    VEqPair u us        -> VEqPair (normal ns u) (normal ns us)
-    VEqJ a u c d x p    -> eqJ (normal ns a) (normal ns u) (normal ns c)
+    VId a u v           -> VId (normal ns a) (normal ns u) (normal ns v)
+    VIdPair u us        -> VIdPair (normal ns u) (normal ns us)
+    VIdJ a u c d x p    -> idJ (normal ns a) (normal ns u) (normal ns c)
                                (normal ns d) (normal ns x) (normal ns p)
     _                   -> v
 

diff --git a/Exp.cf b/Exp.cf
index 29cfb0e8fc0ece5d4b10aa275e36b953bfae68bd..f93cc81c26f531b7ac829a84ff5ab27416368e6e 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -42,9 +42,9 @@ Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "Glue" Exp4 System ;
 GlueElem.     Exp3 ::= "glue" Exp4 System ;
 UnGlueElem.   Exp3 ::= "unglue" Exp4 System ;
-Eq.           Exp3 ::= "Eq" Exp4 Exp4 Exp3 ;
-EqPair.       Exp3 ::= "eqC" Exp4 System ;
-EqJ.          Exp3 ::= "eqJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ;
+Id.           Exp3 ::= "Id" Exp4 Exp4 Exp3 ;
+IdPair.       Exp3 ::= "idC" Exp4 System ;
+IdJ.          Exp3 ::= "idJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ;
 Fst.          Exp4 ::= Exp4 ".1" ;
 Snd.          Exp4 ::= Exp4 ".2" ;
 Pair.         Exp5 ::= "(" Exp "," [Exp] ")" ;

diff --git a/Resolver.hs b/Resolver.hs
index 9cd9890987306c6e5a708a3f92e378a0fe2522c8..c61f65d3957b989b32b10a6ca52de20ee56998de 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -219,9 +219,9 @@ resolveExp e = case e of
   Glue u ts     -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
   GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
   UnGlueElem u ts -> CTT.UnGlueElem <$> resolveExp u <*> resolveSystem ts
-  Eq a u v      -> CTT.Eq <$> resolveExp a <*> resolveExp u <*> resolveExp v
-  EqPair u ts   -> CTT.EqPair <$> resolveExp u <*> resolveSystem ts
-  EqJ a t c d x p -> CTT.EqJ <$> resolveExp a <*> resolveExp t <*> resolveExp c
+  Id a u v      -> CTT.Id <$> resolveExp a <*> resolveExp u <*> resolveExp v
+  IdPair u ts   -> CTT.IdPair <$> resolveExp u <*> resolveSystem ts
+  IdJ a t c d x p -> CTT.IdJ <$> resolveExp a <*> resolveExp t <*> resolveExp c
                              <*> resolveExp d <*> resolveExp x <*> resolveExp p
   _ -> do
     modName <- asks envModule

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 8b74327d24a671e3bb3297adc52ca65f5ee88242..7a038de00252bbdfe9c807839be36dc788646691 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -215,12 +215,12 @@ check a t = case (a,t) of
     check va u\r
     vu <- evalTyping u\r
     checkGlueElemU vu ves us\r
-  (VU,Eq a a0 a1) -> do\r
+  (VU,Id a a0 a1) -> do\r
     check VU a\r
     va <- evalTyping a\r
     check va a0\r
     check va a1\r
-  (VEq va va0 va1,EqPair w ts) -> do\r
+  (VId va va0 va1,IdPair w ts) -> do\r
     check (VPathP (constPath va) va0 va1) w\r
     vw <- evalTyping w\r
     checkSystemWith ts $ \alpha tAlpha ->\r
@@ -498,21 +498,21 @@ infer e = case e of
     checks (bs,nu) es\r
     mapM_ checkFormula phis\r
     return va\r
-  EqJ a u c d x p -> do\r
+  IdJ a u c d x p -> do\r
     check VU a\r
     va <- evalTyping a\r
     check va u\r
     vu <- evalTyping u\r
-    let refu = VEqPair (constPath vu) $ mkSystem [(eps,vu)]\r
+    let refu = VIdPair (constPath vu) $ mkSystem [(eps,vu)]\r
     rho <- asks env\r
     let z = Var "z"\r
-        ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Eq a u z) U\r
+        ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Id a u z) U\r
     check ctype c\r
     vc <- evalTyping c\r
     check (app (app vc vu) refu) d\r
     check va x\r
     vx <- evalTyping x\r
-    check (VEq va vu vx) p\r
+    check (VId va vu vx) p\r
     vp <- evalTyping p\r
     return (app (app vc vx) vp)\r
   _ -> throwError ("infer " ++ show e)\r

diff --git a/examples/eq.ctt b/examples/eq.ctt
index 34f0ea6b0945379aee1c33d5d4f7ca415fc06f06..d0937970123e9eb93677570accecdd94af35f1ab 100644 (file)
--- a/examples/eq.ctt
+++ b/examples/eq.ctt
@@ -2,80 +2,80 @@ module eq where
 
 import prelude
 
-refEq (A : U) (a : A) : Eq A a a =
-  eqC (<i> a) [  -> a ]
+refId (A : U) (a : A) : Id A a a =
+  idC (<i> a) [  -> a ]
 
-JJ (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a))
-   (x : A) (p : Eq A a x) : C x p
-   = eqJ A a C d x p
+JJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refId A a))
+   (x : A) (p : Id A a x) : C x p
+   = idJ A a C d x p
 
-JJref (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a))
-   : C a (refEq A a)
-   = eqJ A a C d a (refEq A a)
+JJref (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refId A a))
+   : C a (refId A a)
+   = idJ A a C d a (refId A a)
 
-JJEq (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a))
-   : Eq (C a (refEq A a)) d (JJ A a C d a (refEq A a))
-   = refEq (C a (refEq A a)) d
+JJId (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refId A a))
+   : Id (C a (refId A a)) d (JJ A a C d a (refId A a))
+   = refId (C a (refId A a)) d
 
-substEq (A : U) (F : A -> U) (a b : A) (p : Eq A a b) (e : F a) : F b =
-  JJ A a (\ (x : A) (_ : Eq A a x) -> F x) e b p
+substId (A : U) (F : A -> U) (a b : A) (p : Id A a b) (e : F a) : F b =
+  JJ A a (\ (x : A) (_ : Id A a x) -> F x) e b p
 
-substEqRef (A : U) (F : A -> U) (a : A) (e : F a) : F a =
-  substEq A F a a (refEq A a) e
+substIdRef (A : U) (F : A -> U) (a : A) (e : F a) : F a =
+  substId A F a a (refId A a) e
 
-transEq (A : U) (a b c : A) (p : Eq A a b) (q : Eq A b c) : Eq A a c =
-  substEq A (\ (z : A) -> Eq A a z) b c q p
+transId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
+  substId A (\ (z : A) -> Id A a z) b c q p
 
-transEqRef (A : U) (a b : A) (p : Eq A a b): Eq A a b =
-  transEq A a a b (refEq A a) p
+transIdRef (A : U) (a b : A) (p : Id A a b): Id A a b =
+  transId A a a b (refId A a) p
 
-eqToId (A : U) (a b : A) (p : Eq A a b) : Id A a b =
-  eqJ A a (\ (b : A) (p : Eq A a b) -> Id A a b)
+idToPath (A : U) (a b : A) (p : Id A a b) : Path A a b =
+  idJ A a (\ (b : A) (p : Id A a b) -> Path A a b)
     (<i> a) b p
 
-idToEq (A : U) (a b : A) (p : Id A a b) : Eq A a b =
---  eqC p []
-  J A a (\ (b : A) (p : Id A a b) -> Eq A a b)
-    (refEq A a) b p
+idToId (A : U) (a b : A) (p : Path A a b) : Id A a b =
+--  idC p []
+  J A a (\ (b : A) (p : Path A a b) -> Id A a b)
+    (refId A a) b p
 
-idToEqRef (A : U) (a : A) : Id (Eq A a a) (refEq A a) (idToEq A a a (<_> a)) =
-  JEq A a (\ (b : A) (p : Id A a b) -> Eq A a b) (refEq A a)
+idToIdRef (A : U) (a : A) : Path (Id A a a) (refId A a) (idToId A a a (<_> a)) =
+  JEq A a (\ (b : A) (p : Path A a b) -> Id A a b) (refId A a)
 
-eqToIdRef (A : U) (a : A) : Id (Id A a a) (<_> a) (eqToId A a a (refEq A a)) =
+idToPathRef (A : U) (a : A) : Path (Path A a a) (<_> a) (idToPath A a a (refId A a)) =
   <i j> a
   
 
-idToEqToId (A : U) (a b : A) (p : Id A a b) :
-  Id (Id A a b) p (eqToId A a b (idToEq A a b p)) =
-  J A a (\ (b : A) (p : Id A a b) ->
-    Id (Id A a b) p (eqToId A a b (idToEq A a b p)))
-    (<j> eqToId A a a (idToEqRef A a @ j)) b p
+idToIdToPath (A : U) (a b : A) (p : Path A a b) :
+  Path (Path A a b) p (idToPath A a b (idToId A a b p)) =
+  J A a (\ (b : A) (p : Path A a b) ->
+    Path (Path A a b) p (idToPath A a b (idToId A a b p)))
+    (<j> idToPath A a a (idToIdRef A a @ j)) b p
 
 lem (A : U) (a : A) :
-  Id (Eq A a a) (refEq A a) (idToEq A a a (eqToId A a a (refEq A a))) =
-    compId (Eq A a a)
-      (refEq A a) (idToEq A a a (<_> a)) (idToEq A a a (eqToId A a a (refEq A a)))
-      (idToEqRef A a) (<k> idToEq A a a (eqToIdRef A a @ k))
-
-eqToIdToEq (A : U) (a b : A) (p : Eq A a b) :
-  Id (Eq A a b) p (idToEq A a b (eqToId A a b p)) =
-  eqJ A a (\ (b : A) (p : Eq A a b) ->
-    Id (Eq A a b) p (idToEq A a b (eqToId A a b p)))
+  Path (Id A a a) (refId A a) (idToId A a a (idToPath A a a (refId A a))) =
+    compPath (Id A a a)
+      (refId A a) (idToId A a a (<_> a)) (idToId A a a (idToPath A a a (refId A a)))
+      (idToIdRef A a) (<k> idToId A a a (idToPathRef A a @ k))
+
+idToPathToId (A : U) (a b : A) (p : Id A a b) :
+  Path (Id A a b) p (idToId A a b (idToPath A a b p)) =
+  idJ A a (\ (b : A) (p : Id A a b) ->
+    Path (Id A a b) p (idToId A a b (idToPath A a b p)))
     (lem A a) b p
 
 
 --------------------------------------------------------------------------------
 -- Some tests
 
-mop (A B : U) (f : A -> B) (u v : A) (p : Eq A u v) : Eq B (f u) (f v) =
-  JJ A u (\ (v : A) (p : Eq A u v) -> Eq B (f u) (f v))
-    (refEq B (f u)) v p
+mop (A B : U) (f : A -> B) (u v : A) (p : Id A u v) : Id B (f u) (f v) =
+  JJ A u (\ (v : A) (p : Id A u v) -> Id B (f u) (f v))
+    (refId B (f u)) v p
 
-mopComp (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Eq A u v)
-  : Eq C (g (f u)) (g (f v)) = mop A C (\ (x : A) -> g (f x)) u v p
+mopComp (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Id A u v)
+  : Id C (g (f u)) (g (f v)) = mop A C (\ (x : A) -> g (f x)) u v p
 
-mopComp' (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Eq A u v)
-  : Eq C (g (f u)) (g (f v)) = mop B C g (f u) (f v) (mop A B f u v p)
+mopComp' (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Id A u v)
+  : Id C (g (f u)) (g (f v)) = mop B C g (f u) (f v) (mop A B f u v p)
 
-superMop (A B : U) (f : A -> B) (u v : A) (p : Id A u v) : Eq B (f u) (f v) =
-  eqC (<i> f (p @ i)) [ ]
+superMop (A B : U) (f : A -> B) (u v : A) (p : Path A u v) : Id B (f u) (f v) =
+  idC (<i> f (p @ i)) [ ]