Make normal print nicer names

diff --git a/CTT.hs b/CTT.hs
index 5b15f7ecedcd90fa6d9be29683f0ba058965c650..0d5bf49ebeb496be7746d39cb6e4f8a6ba107c1c 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -213,6 +213,10 @@ isNeutralComp _ _ _ = False
 mkVar :: Int -> String -> Val -> Val
 mkVar k x = VVar (x ++ show k)
 
+mkVarNice :: [String] -> String -> Val -> Val
+mkVarNice xs x = VVar (head (ys \\ xs))
+  where ys = x:map (\n -> x ++ show n) [0..]
+
 unCon :: Val -> [Val]
 unCon (VCon _ vs) = vs
 unCon v           = error $ "unCon: not a constructor: " ++ show v

diff --git a/Eval.hs b/Eval.hs
index 7869b9283bb0385382def98a24f01aa90e5c062a..0f7bbdc98100c8e769bebdc75fefeae6d91ed48d 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -786,48 +786,48 @@ instance Convertible Formula where
 -- | Normalization
 
 class Normal a where
-  normal :: Int -> a -> a
+  normal :: [String] -> a -> a
 
 -- Does neither normalize formulas nor environments.
 instance Normal Val where
-  normal k v = case v of
+  normal ns v = case v of
     VU                  -> VU
     Ter (Lam x t u) e   -> let w = eval e t
-                               v@(VVar name _) = mkVar k x w
-                           in VLam name (normal k w) $ normal (k+1) (eval (Upd e (x,v)) u)
-    VPi u v             -> VPi (normal k u) (normal k v)
-    VSigma u v          -> VSigma (normal k u) (normal k v)
-    VPair u v           -> VPair (normal k u) (normal k v)
-    VCon n us           -> VCon n (normal k us)
-    VPCon n u us phis   -> VPCon n (normal k u) (normal k us) phis
-    VIdP a u0 u1        -> VIdP (normal k a) (normal k u0) (normal k u1)
-    VPath i u           -> VPath i (normal k u)
-    VComp u v vs        -> compLine (normal k u) (normal k v) (normal k vs)
-    VTrans u v          -> transLine (normal k u) (normal k v)
-    VGlue u hisos       -> glue (normal k u) (normal k hisos)
-    VGlueElem u us      -> glueElem (normal k u) (normal k us)
-    VCompElem a es u us -> compElem (normal k a) (normal k es) (normal k u) (normal k us)
-    VElimComp a es u    -> elimComp (normal k a) (normal k es) (normal k u)
-    VVar x t            -> VVar x t -- (normal k t)
-    VFst t              -> fstVal (normal k t)
-    VSnd t              -> sndVal (normal k t)
-    VSplit u t          -> VSplit (normal k u) (normal k t)
-    VApp u v            -> app (normal k u) (normal k v)
-    VAppFormula u phi   -> VAppFormula (normal k u) phi
+                               v@(VVar n _) = mkVarNice ns x w
+                           in VLam n (normal ns w) $ normal (n:ns) (eval (Upd e (x,v)) u)
+    VPi u v             -> VPi (normal ns u) (normal ns v)
+    VSigma u v          -> VSigma (normal ns u) (normal ns v)
+    VPair u v           -> VPair (normal ns u) (normal ns v)
+    VCon n us           -> VCon n (normal ns us)
+    VPCon n u us phis   -> VPCon n (normal ns u) (normal ns us) phis
+    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)
+    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)
+    VVar x t            -> VVar x t -- (normal ns t)
+    VFst t              -> fstVal (normal ns t)
+    VSnd t              -> sndVal (normal ns t)
+    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) phi
     _                   -> v
 
 instance Normal a => Normal (Map k a) where
-  normal k us = Map.map (normal k) us
+  normal ns us = Map.map (normal ns) us
 
 instance (Normal a,Normal b) => Normal (a,b) where
-  normal k (u,v) = (normal k u,normal k v)
+  normal ns (u,v) = (normal ns u,normal ns v)
 
 instance (Normal a,Normal b,Normal c) => Normal (a,b,c) where
-  normal k (u,v,w) = (normal k u,normal k v,normal k w)
+  normal ns (u,v,w) = (normal ns u,normal ns v,normal ns w)
 
 instance (Normal a,Normal b,Normal c,Normal d) => Normal (a,b,c,d) where
-  normal k (u,v,w,x) =
-    (normal k u,normal k v,normal k w, normal k x)
+  normal ns (u,v,w,x) =
+    (normal ns u,normal ns v,normal ns w, normal ns x)
 
 instance Normal a => Normal [a] where
-  normal k us = map (normal k) us
+  normal ns us = map (normal ns) us

diff --git a/Main.hs b/Main.hs
index e90edcfd3b4f31272ae2510f8d3ba012e62d3118..0dee3c0d1b14e7e4d0264e32576a4aeeed0d0d45 100644 (file)
--- a/Main.hs
+++ b/Main.hs
@@ -116,7 +116,7 @@ loop flags f names tenv = do
     Just str'  ->
       let (msg,str,mod) = case str' of
             (':':'n':' ':str) ->
-              ("NORMEVAL: ",str,E.normal 0)
+              ("NORMEVAL: ",str,E.normal [])
             str -> ("EVAL: ",str,id)
       in case pExp (lexer str) of
       Bad err -> outputStrLn ("Parse error: " ++ err) >> loop flags f names tenv

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 06ce964cbef6c37762ea9246bf1e40ae0e8ead2d..bd5ea08ca1fe6e991ac786705865bc3757ad7fd3 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -149,9 +149,10 @@ check a t = case (a,t) of
   (_,Hole l)  -> do\r
       rho <- asks env\r
       let e = unlines (reverse (contextOfEnv rho))\r
-      k <- asks index\r
+--      k <- asks index\r
+      -- TODO: Fix\r
       trace $ "\nHole at " ++ show l ++ ":\n\n" ++\r
-              e ++ replicate 80 '-' ++ "\n" ++ show (normal k a)  ++ "\n"\r
+              e ++ replicate 80 '-' ++ "\n" ++ show (normal [] a)  ++ "\n"\r
   (_,Con c es) -> do\r
     (bs,nu) <- getLblType c a\r
     checks (bs,nu) es\r

diff --git a/examples/prop.ctt b/examples/prop.ctt
index fe6cf7ca4934ecd04fe664e5bfc2f52f6663d174..cb6d02cdcec5593a646bdc1ef4c2c9253c54a7bb 100644 (file)
--- a/examples/prop.ctt
+++ b/examples/prop.ctt
@@ -8,20 +8,18 @@ lemProp (A B : U) (f : A -> B) (g : B -> A)
  \ (b0 b1:B) -> subst U prop A B (isoId A B f g s t) pA b0 b1
 
 {- normal form
- 
-\(A0 : U) -> \(B1 : U) -> \(f2 : A0 -> B1) -> \(g3 : B1 -> A0) -> 
- \(s4 : \(y4 : B1) -> IdP (<i> B1) (f2 (g3 y4)) y4) -> 
- \(t5 : \(x5 : A0) -> IdP (<i> A0) (g3 (f2 x5)) x5) ->
- \(pA6 : \(a6 : A0) -> \(b7 : A0) -> IdP (<i> A0) a6 b7) ->
- \(b07 : B1) -> \(b18 : B1) ->
- <j> comp B1 (f2 ((pA6 (g3 b07) (g3 b18)) @ j))
-  [ (j = 0) -> <i> comp B1 b07 
-                [ (i = 0) -> <j> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> <i> (t5 (g3 b07)) @ -i ]))
-                                         [ (j = 0) -> <i> (s4 b07) @ i, (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] 
+\(A : U) -> \(B : U) -> \(f : A -> B) -> \(g : B -> A) ->
+ \(s : \(y : B) -> IdP (<i> B) (f (g y)) y) ->
+ \(t : \(x : A) -> IdP (<i> A) (g (f x)) x) ->
+ \(pA : \(a : A) -> \(b : A) -> IdP (<i> A) a b) ->
+ \(b0 : B) -> \(b1 : B) ->
+ <j> comp B (f (pA (g b0) (g b1) @ j))
+  [ (j = 0) -> <i> comp B b0
+                [ (i = 0) -> <j> comp B (f (comp A (g b0) [ (j = 1) -> <i> t (g b0) @ -i ]))
+                                        [ (j = 0) -> <i> s b0 @ i, (j = 1) -> <i> s (f (g b0)) @ i ]
                 ]
-  , (j = 1) -> <i> comp B1 b18 [ (i = 0) -> <j> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> <i> (t5 (g3 b18)) @ -i ])) 
-                                                [ (j = 0) -> <i> (s4 b18) @ i, (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] 
-                               ] 
+  , (j = 1) -> <i> comp B b1 [ (i = 0) -> <j> comp B (f (comp A (g b1) [ (j = 1) -> <i> t (g b1) @ -i ]))
+                                              [ (j = 0) -> <i> s b1 @ i, (j = 1) -> <i> s (f (g b1)) @ i ] ]
   ]
 -}
 
@@ -31,11 +29,10 @@ lemSet (A B : U) (f : A -> B) (g : B -> A)
  \ (b0 b1:B) (p q : Id B b0 b1) -> subst U set A B (isoId A B f g s t) sA b0 b1 p q
 
 {- normal form
- \(A0 : U) -> \(B1 : U) -> 
- \(f2 : A0 -> B1) -> \(g3 : B1 -> A0) -> 
- \(s4 : \(y4 : B1) -> IdP (<i> B1) (f2 (g3 y4)) y4) -> 
- \(t5 : \(x5 : A0) -> IdP (<i> A0) (g3 (f2 x5)) x5) -> 
- \(sA6 : \(a6 : A0) -> \(b7 : A0) -> \(a8 : IdP (<i> A0) a6 b7) -> \(b9 : IdP (<i> A0) a6 b7) -> IdP (<i> IdP (<i> A0) a6 b7) a8 b9) -> 
- \(b07 : B1) -> \(b18 : B1) -> \(p9 : IdP (<i> B1) b07 b18) -> \(q10 : IdP (<i> B1) b07 b18) -> 
- <j> <k> comp B1 (comp B1 (f2 (((sA6 (g3 b07) (g3 b18) (<j> comp A0 (g3 (p9 @ j)) [ (j = 0) -> <i> comp A0 (g3 (comp B1 b07 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> <i> (s4 b07) @ i, (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b07)) @ j ], (j = 1) -> <i> comp A0 (g3 (comp B1 b18 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> <i> (s4 b18) @ i, (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b18)) @ j ] ]) (<j> comp A0 (g3 (q10 @ j)) [ (j = 0) -> <i> comp A0 (g3 (comp B1 b07 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> <i> (s4 b07) @ i, (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b07)) @ j ], (j = 1) -> <i> comp A0 (g3 (comp B1 b18 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> <i> (s4 b18) @ i, (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b18)) @ j ] ])) @ j) @ k)) [ (k = 0) -> <i> comp B1 b07 [ (i = 0) -> <j> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> <i> (s4 b07) @ i, (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ], (k = 1) -> <i> comp B1 b18 [ (i = 0) -> <j> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> <i> (s4 b18) @ i, (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ] ]) [ (j = 0) -> <i> comp B1 (comp B1 (comp B1 (comp B1 (p9 @ k) [ (i = 0) -> <j> comp B1 (f2 (comp A0 (g3 (p9 @ k)) [ (j = 1) -> <i> (t5 (g3 (p9 @ k))) @ -i ])) [ (j = 0) -> <i> (s4 (p9 @ k)) @ i, (j = 1) -> <i> (s4 (f2 (g3 (p9 @ k)))) @ i ] ]) [ (k = 0) -> <j> comp B1 (comp B1 b07 [ (i = 0)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ]) [ (i = 0) -> <k> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b07)) @ (k /\ i) ]) [ (j = 1) -> <i> (t5 (g3 b07)) @ (k /\ -i), (k = 1) -> <i> (t5 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b07)) @ i ])) @ -i ])) [ (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i, (k = 0) -> <i> (s4 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) @ i, (k = 1) -> <i> (s4 (f2 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b07)) @ i ]))) @ i ] ], (k = 1) -> <j> comp B1 (comp B1 b18 [ (i = 0)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ]) [ (i = 0) -> <k> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b18)) @ (k /\ i) ]) [ (j = 1) -> <i> (t5 (g3 b18)) @ (k /\ -i), (k = 1) -> <i> (t5 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b18)) @ i ])) @ -i ])) [ (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i, (k = 0) -> <i> (s4 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) @ i, (k = 1) -> <i> (s4 (f2 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b18)) @ i ]))) @ i ] ] ]) [ (i = 0) -> <j> comp B1 (f2 (g3 (p9 @ k))) [ (j = 0) -> <i> comp B1 (f2 (g3 (p9 @ k))) [ (k = 0) -> <j> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b07)) @ k ]), (k = 1) -> <j> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b18)) @ k ]) ], (j = 1) -> <i> f2 (comp A0 (g3 (p9 @ k)) [ (k = 0) -> <j> comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b07)) @ k ], (k = 1) -> <j> comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b18)) @ k ] ]), (k = 0) -> <i> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> <i> (s4 b07) @ i, (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b07)) @ j ]), (k = 1) -> <i> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> <i> (s4 b18) @ i, (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b18)) @ j ]) ] ]) [ (k = 0) -> <j> comp B1 b07 [ (i = 0)(j = 0) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ], (k = 1) -> <j> comp B1 b18 [ (i = 0)(j = 0) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ] ], (j = 1) -> <i> comp B1 (comp B1 (comp B1 (comp B1 (q10 @ k) [ (i = 0) -> <j> comp B1 (f2 (comp A0 (g3 (q10 @ k)) [ (j = 1) -> <i> (t5 (g3 (q10 @ k))) @ -i ])) [ (j = 0) -> <i> (s4 (q10 @ k)) @ i, (j = 1) -> <i> (s4 (f2 (g3 (q10 @ k)))) @ i ] ]) [ (k = 0) -> <j> comp B1 (comp B1 b07 [ (i = 0)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ]) [ (i = 0) -> <k> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b07)) @ (k /\ i) ]) [ (j = 1) -> <i> (t5 (g3 b07)) @ (k /\ -i), (k = 1) -> <i> (t5 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b07)) @ i ])) @ -i ])) [ (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i, (k = 0) -> <i> (s4 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) @ i, (k = 1) -> <i> (s4 (f2 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> <j> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> <j> (s4 b07) @ j, (i = 1) -> <j> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b07)) @ i ]))) @ i ] ], (k = 1) -> <j> comp B1 (comp B1 b18 [ (i = 0)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ]) [ (i = 0) -> <k> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b18)) @ (k /\ i) ]) [ (j = 1) -> <i> (t5 (g3 b18)) @ (k /\ -i), (k = 1) -> <i> (t5 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b18)) @ i ])) @ -i ])) [ (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i, (k = 0) -> <i> (s4 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) @ i, (k = 1) -> <i> (s4 (f2 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> <i> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> <j> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> <j> (s4 b18) @ j, (i = 1) -> <j> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> <i> (t5 (g3 b18)) @ i ]))) @ i ] ] ]) [ (i = 0) -> <j> comp B1 (f2 (g3 (q10 @ k))) [ (j = 0) -> <i> comp B1 (f2 (g3 (q10 @ k))) [ (k = 0) -> <j> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b07)) @ k ]), (k = 1) -> <j> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b18)) @ k ]) ], (j = 1) -> <i> f2 (comp A0 (g3 (q10 @ k)) [ (k = 0) -> <j> comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b07)) @ k ], (k = 1) -> <j> comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> <k> (t5 (g3 b18)) @ k ] ]), (k = 0) -> <i> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> <i> (s4 b07) @ i, (j = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b07)) @ j ]), (k = 1) -> <i> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1) -> <j> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> <i> (s4 b18) @ i, (j = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> <j> (t5 (g3 b18)) @ j ]) ] ]) [ (k = 0) -> <j> comp B1 b07 [ (i = 0)(j = 0) -> <k> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> <i> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> <i> (s4 b07) @ i, (k = 1) -> <i> (s4 (f2 (g3 b07))) @ i ] ], (k = 1) -> <j> comp B1 b18 [ (i = 0)(j = 0) -> <k> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> <i> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> <i> (s4 b18) @ i, (k = 1) -> <i> (s4 (f2 (g3 b18))) @ i ] ] ] ] 
+\(A : U) -> \(B : U) ->
+  \(f : A -> B) -> \(g : B -> A) ->
+  \(s : \(y : B) -> IdP (<i> B) (f (g y)) y) ->
+  \(t : \(x : A) -> IdP (<i> A) (g (f x)) x) ->
+  \(sA : \(a : A) -> \(b : A) -> \(a0 : IdP (<i> A) a b) -> \(b0 : IdP (<i> A) a b) -> IdP (<i> IdP (<i> A) a b) a0 b0) -> \(b0 : B) -> \(b1 : B) -> \(p : IdP (<i> B) b0 b1) -> \(q : IdP (<i> B) b0 b1) ->
+  <j> <k> comp B (comp B (f (sA (g b0) (g b1) (<j> comp A (g (p @ j)) [ (j = 0) -> <i> comp A (g (comp B b0 [ (i = 1) -> <j> comp B (f (comp A (g b0) [ (j = 1) -> <i> t (g b0) @ -i ])) [ (j = 0) -> <i> s b0 @ i, (j = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1) -> <j> t (g b0) @ j ], (j = 1) -> <i> comp A (g (comp B b1 [ (i = 1) -> <j> comp B (f (comp A (g b1) [ (j = 1) -> <i> t (g b1) @ -i ])) [ (j = 0) -> <i> s b1 @ i, (j = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1) -> <j> t (g b1) @ j ] ]) (<j> comp A (g (q @ j)) [ (j = 0) -> <i> comp A (g (comp B b0 [ (i = 1) -> <j> comp B (f (comp A (g b0) [ (j = 1) -> <i> t (g b0) @ -i ])) [ (j = 0) -> <i> s b0 @ i, (j = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1) -> <j> t (g b0) @ j ], (j = 1) -> <i> comp A (g (comp B b1 [ (i = 1) -> <j> comp B (f (comp A (g b1) [ (j = 1) -> <i> t (g b1) @ -i ])) [ (j = 0) -> <i> s b1 @ i, (j = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1) -> <j> t (g b1) @ j ] ]) @ j @ k)) [ (k = 0) -> <i> comp B b0 [ (i = 0) -> <j> comp B (f (comp A (g b0) [ (j = 1) -> <i> t (g b0) @ -i ])) [ (j = 0) -> <i> s b0 @ i, (j = 1) -> <i> s (f (g b0)) @ i ] ], (k = 1) -> <i> comp B b1 [ (i = 0) -> <j> comp B (f (comp A (g b1) [ (j = 1) -> <i> t (g b1) @ -i ])) [ (j = 0) -> <i> s b1 @ i, (j = 1) -> <i> s (f (g b1)) @ i ] ] ]) [ (j = 0) -> <i> comp B (comp B (comp B (comp B (p @ k) [ (i = 0) -> <j> comp B (f (comp A (g (p @ k)) [ (j = 1) -> <i> t (g (p @ k)) @ -i ])) [ (j = 0) -> <i> s (p @ k) @ i, (j = 1) -> <i> s (f (g (p @ k))) @ i ] ]) [ (k = 0) -> <j> comp B (comp B b0 [ (i = 0)(j = 1) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ]) [ (i = 0) -> <k> comp B (f (comp A (comp A (g (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ])) [ (j = 1) -> <i> t (g b0) @ (k /\ i) ]) [ (j = 1) -> <i> t (g b0) @ (k /\ -i), (k = 1) -> <i> t (comp A (g (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ])) [ (j = 1) -> <i> t (g b0) @ i ]) @ -i ])) [ (j = 1) -> <i> s (f (g b0)) @ i, (k = 0) -> <i> s (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ]) @ i, (k = 1) -> <i> s (f (comp A (g (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ])) [ (j = 1) -> <i> t (g b0) @ i ])) @ i ] ], (k = 1) -> <j> comp B (comp B b1 [ (i = 0)(j = 1) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ]) [ (i = 0) -> <k> comp B (f (comp A (comp A (g (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ])) [ (j = 1) -> <i> t (g b1) @ (k /\ i) ]) [ (j = 1) -> <i> t (g b1) @ (k /\ -i), (k = 1) -> <i> t (comp A (g (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ])) [ (j = 1) -> <i> t (g b1) @ i ]) @ -i ])) [ (j = 1) -> <i> s (f (g b1)) @ i, (k = 0) -> <i> s (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ]) @ i, (k = 1) -> <i> s (f (comp A (g (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ])) [ (j = 1) -> <i> t (g b1) @ i ])) @ i ] ] ]) [ (i = 0) -> <j> comp B (f (g (p @ k))) [ (j = 0) -> <i> comp B (f (g (p @ k))) [ (k = 0) -> <j> f (comp A (g (comp B b0 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b0) @ k ]), (k = 1) -> <j> f (comp A (g (comp B b1 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b1) @ k ]) ], (j = 1) -> <i> f (comp A (g (p @ k)) [ (k = 0) -> <j> comp A (g (comp B b0 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b0) @ k ], (k = 1) -> <j> comp A (g (comp B b1 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b1) @ k ] ]), (k = 0) -> <i> f (comp A (g (comp B b0 [ (i = 1) -> <j> comp B (f (comp A (g b0) [ (j = 1) -> <i> t (g b0) @ -i ])) [ (j = 0) -> <i> s b0 @ i, (j = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1) -> <j> t (g b0) @ j ]), (k = 1) -> <i> f (comp A (g (comp B b1 [ (i = 1) -> <j> comp B (f (comp A (g b1) [ (j = 1) -> <i> t (g b1) @ -i ])) [ (j = 0) -> <i> s b1 @ i, (j = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1) -> <j> t (g b1) @ j ]) ] ]) [ (k = 0) -> <j> comp B b0 [ (i = 0)(j = 0) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ], (k = 1) -> <j> comp B b1 [ (i = 0)(j = 0) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ] ], (j = 1) -> <i> comp B (comp B (comp B (comp B (q @ k) [ (i = 0) -> <j> comp B (f (comp A (g (q @ k)) [ (j = 1) -> <i> t (g (q @ k)) @ -i ])) [ (j = 0) -> <i> s (q @ k) @ i, (j = 1) -> <i> s (f (g (q @ k))) @ i ] ]) [ (k = 0) -> <j> comp B (comp B b0 [ (i = 0)(j = 1) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ]) [ (i = 0) -> <k> comp B (f (comp A (comp A (g (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ])) [ (j = 1) -> <i> t (g b0) @ (k /\ i) ]) [ (j = 1) -> <i> t (g b0) @ (k /\ -i), (k = 1) -> <i> t (comp A (g (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ])) [ (j = 1) -> <i> t (g b0) @ i ]) @ -i ])) [ (j = 1) -> <i> s (f (g b0)) @ i, (k = 0) -> <i> s (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ]) @ i, (k = 1) -> <i> s (f (comp A (g (comp B b0 [ (j = 1) -> <i> comp B (f (comp A (g b0) [ (i = 1) -> <j> t (g b0) @ -j ])) [ (i = 0) -> <j> s b0 @ j, (i = 1) -> <j> s (f (g b0)) @ j ] ])) [ (j = 1) -> <i> t (g b0) @ i ])) @ i ] ], (k = 1) -> <j> comp B (comp B b1 [ (i = 0)(j = 1) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ]) [ (i = 0) -> <k> comp B (f (comp A (comp A (g (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ])) [ (j = 1) -> <i> t (g b1) @ (k /\ i) ]) [ (j = 1) -> <i> t (g b1) @ (k /\ -i), (k = 1) -> <i> t (comp A (g (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ])) [ (j = 1) -> <i> t (g b1) @ i ]) @ -i ])) [ (j = 1) -> <i> s (f (g b1)) @ i, (k = 0) -> <i> s (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ]) @ i, (k = 1) -> <i> s (f (comp A (g (comp B b1 [ (j = 1) -> <i> comp B (f (comp A (g b1) [ (i = 1) -> <j> t (g b1) @ -j ])) [ (i = 0) -> <j> s b1 @ j, (i = 1) -> <j> s (f (g b1)) @ j ] ])) [ (j = 1) -> <i> t (g b1) @ i ])) @ i ] ] ]) [ (i = 0) -> <j> comp B (f (g (q @ k))) [ (j = 0) -> <i> comp B (f (g (q @ k))) [ (k = 0) -> <j> f (comp A (g (comp B b0 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b0) @ k ]), (k = 1) -> <j> f (comp A (g (comp B b1 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b1) @ k ]) ], (j = 1) -> <i> f (comp A (g (q @ k)) [ (k = 0) -> <j> comp A (g (comp B b0 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b0) @ k ], (k = 1) -> <j> comp A (g (comp B b1 [ (i = 1)(j = 1) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> <k> t (g b1) @ k ] ]), (k = 0) -> <i> f (comp A (g (comp B b0 [ (i = 1) -> <j> comp B (f (comp A (g b0) [ (j = 1) -> <i> t (g b0) @ -i ])) [ (j = 0) -> <i> s b0 @ i, (j = 1) -> <i> s (f (g b0)) @ i ] ])) [ (i = 1) -> <j> t (g b0) @ j ]), (k = 1) -> <i> f (comp A (g (comp B b1 [ (i = 1) -> <j> comp B (f (comp A (g b1) [ (j = 1) -> <i> t (g b1) @ -i ])) [ (j = 0) -> <i> s b1 @ i, (j = 1) -> <i> s (f (g b1)) @ i ] ])) [ (i = 1) -> <j> t (g b1) @ j ]) ] ]) [ (k = 0) -> <j> comp B b0 [ (i = 0)(j = 0) -> <k> comp B (f (comp A (g b0) [ (k = 1) -> <i> t (g b0) @ -i ])) [ (k = 0) -> <i> s b0 @ i, (k = 1) -> <i> s (f (g b0)) @ i ] ], (k = 1) -> <j> comp B b1 [ (i = 0)(j = 0) -> <k> comp B (f (comp A (g b1) [ (k = 1) -> <i> t (g b1) @ -i ])) [ (k = 0) -> <i> s b1 @ i, (k = 1) -> <i> s (f (g b1)) @ i ] ] ] ]
 -}