From: Anders Date: Mon, 20 Apr 2015 15:07:21 +0000 (+0200) Subject: Make normal print nicer names X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=07ec799f068e61c98475f933650a70d51c14e042;p=cubicaltt.git Make normal print nicer names --- diff --git a/CTT.hs b/CTT.hs index 5b15f7e..0d5bf49 100644 --- 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 7869b92..0f7bbdc 100644 --- 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 e90edcf..0dee3c0 100644 --- 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 06ce964..bd5ea08 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -149,9 +149,10 @@ check a t = case (a,t) of (_,Hole l) -> do rho <- asks env let e = unlines (reverse (contextOfEnv rho)) - k <- asks index +-- k <- asks index + -- TODO: Fix trace $ "\nHole at " ++ show l ++ ":\n\n" ++ - e ++ replicate 80 '-' ++ "\n" ++ show (normal k a) ++ "\n" + e ++ replicate 80 '-' ++ "\n" ++ show (normal [] a) ++ "\n" (_,Con c es) -> do (bs,nu) <- getLblType c a checks (bs,nu) es diff --git a/examples/prop.ctt b/examples/prop.ctt index fe6cf7c..cb6d02c 100644 --- 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 ( B1) (f2 (g3 y4)) y4) -> - \(t5 : \(x5 : A0) -> IdP ( A0) (g3 (f2 x5)) x5) -> - \(pA6 : \(a6 : A0) -> \(b7 : A0) -> IdP ( A0) a6 b7) -> - \(b07 : B1) -> \(b18 : B1) -> - comp B1 (f2 ((pA6 (g3 b07) (g3 b18)) @ j)) - [ (j = 0) -> comp B1 b07 - [ (i = 0) -> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> (t5 (g3 b07)) @ -i ])) - [ (j = 0) -> (s4 b07) @ i, (j = 1) -> (s4 (f2 (g3 b07))) @ i ] +\(A : U) -> \(B : U) -> \(f : A -> B) -> \(g : B -> A) -> + \(s : \(y : B) -> IdP ( B) (f (g y)) y) -> + \(t : \(x : A) -> IdP ( A) (g (f x)) x) -> + \(pA : \(a : A) -> \(b : A) -> IdP ( A) a b) -> + \(b0 : B) -> \(b1 : B) -> + comp B (f (pA (g b0) (g b1) @ j)) + [ (j = 0) -> comp B b0 + [ (i = 0) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) + [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ] - , (j = 1) -> comp B1 b18 [ (i = 0) -> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> (t5 (g3 b18)) @ -i ])) - [ (j = 0) -> (s4 b18) @ i, (j = 1) -> (s4 (f2 (g3 b18))) @ i ] - ] + , (j = 1) -> comp B b1 [ (i = 0) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) + [ (j = 0) -> s b1 @ i, (j = 1) -> 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 ( B1) (f2 (g3 y4)) y4) -> - \(t5 : \(x5 : A0) -> IdP ( A0) (g3 (f2 x5)) x5) -> - \(sA6 : \(a6 : A0) -> \(b7 : A0) -> \(a8 : IdP ( A0) a6 b7) -> \(b9 : IdP ( A0) a6 b7) -> IdP ( IdP ( A0) a6 b7) a8 b9) -> - \(b07 : B1) -> \(b18 : B1) -> \(p9 : IdP ( B1) b07 b18) -> \(q10 : IdP ( B1) b07 b18) -> - comp B1 (comp B1 (f2 (((sA6 (g3 b07) (g3 b18) ( comp A0 (g3 (p9 @ j)) [ (j = 0) -> comp A0 (g3 (comp B1 b07 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> (s4 b07) @ i, (j = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> (t5 (g3 b07)) @ j ], (j = 1) -> comp A0 (g3 (comp B1 b18 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> (s4 b18) @ i, (j = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> (t5 (g3 b18)) @ j ] ]) ( comp A0 (g3 (q10 @ j)) [ (j = 0) -> comp A0 (g3 (comp B1 b07 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> (s4 b07) @ i, (j = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> (t5 (g3 b07)) @ j ], (j = 1) -> comp A0 (g3 (comp B1 b18 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> (s4 b18) @ i, (j = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> (t5 (g3 b18)) @ j ] ])) @ j) @ k)) [ (k = 0) -> comp B1 b07 [ (i = 0) -> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> (s4 b07) @ i, (j = 1) -> (s4 (f2 (g3 b07))) @ i ] ], (k = 1) -> comp B1 b18 [ (i = 0) -> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> (s4 b18) @ i, (j = 1) -> (s4 (f2 (g3 b18))) @ i ] ] ]) [ (j = 0) -> comp B1 (comp B1 (comp B1 (comp B1 (p9 @ k) [ (i = 0) -> comp B1 (f2 (comp A0 (g3 (p9 @ k)) [ (j = 1) -> (t5 (g3 (p9 @ k))) @ -i ])) [ (j = 0) -> (s4 (p9 @ k)) @ i, (j = 1) -> (s4 (f2 (g3 (p9 @ k)))) @ i ] ]) [ (k = 0) -> comp B1 (comp B1 b07 [ (i = 0)(j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ]) [ (i = 0) -> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> (t5 (g3 b07)) @ (k /\ i) ]) [ (j = 1) -> (t5 (g3 b07)) @ (k /\ -i), (k = 1) -> (t5 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> (t5 (g3 b07)) @ i ])) @ -i ])) [ (j = 1) -> (s4 (f2 (g3 b07))) @ i, (k = 0) -> (s4 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) @ i, (k = 1) -> (s4 (f2 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> (t5 (g3 b07)) @ i ]))) @ i ] ], (k = 1) -> comp B1 (comp B1 b18 [ (i = 0)(j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ]) [ (i = 0) -> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> (t5 (g3 b18)) @ (k /\ i) ]) [ (j = 1) -> (t5 (g3 b18)) @ (k /\ -i), (k = 1) -> (t5 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> (t5 (g3 b18)) @ i ])) @ -i ])) [ (j = 1) -> (s4 (f2 (g3 b18))) @ i, (k = 0) -> (s4 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) @ i, (k = 1) -> (s4 (f2 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> (t5 (g3 b18)) @ i ]))) @ i ] ] ]) [ (i = 0) -> comp B1 (f2 (g3 (p9 @ k))) [ (j = 0) -> comp B1 (f2 (g3 (p9 @ k))) [ (k = 0) -> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b07)) @ k ]), (k = 1) -> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b18)) @ k ]) ], (j = 1) -> f2 (comp A0 (g3 (p9 @ k)) [ (k = 0) -> comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b07)) @ k ], (k = 1) -> comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b18)) @ k ] ]), (k = 0) -> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> (s4 b07) @ i, (j = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> (t5 (g3 b07)) @ j ]), (k = 1) -> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> (s4 b18) @ i, (j = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> (t5 (g3 b18)) @ j ]) ] ]) [ (k = 0) -> comp B1 b07 [ (i = 0)(j = 0) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ], (k = 1) -> comp B1 b18 [ (i = 0)(j = 0) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ] ], (j = 1) -> comp B1 (comp B1 (comp B1 (comp B1 (q10 @ k) [ (i = 0) -> comp B1 (f2 (comp A0 (g3 (q10 @ k)) [ (j = 1) -> (t5 (g3 (q10 @ k))) @ -i ])) [ (j = 0) -> (s4 (q10 @ k)) @ i, (j = 1) -> (s4 (f2 (g3 (q10 @ k)))) @ i ] ]) [ (k = 0) -> comp B1 (comp B1 b07 [ (i = 0)(j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ]) [ (i = 0) -> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> (t5 (g3 b07)) @ (k /\ i) ]) [ (j = 1) -> (t5 (g3 b07)) @ (k /\ -i), (k = 1) -> (t5 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> (t5 (g3 b07)) @ i ])) @ -i ])) [ (j = 1) -> (s4 (f2 (g3 b07))) @ i, (k = 0) -> (s4 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) @ i, (k = 1) -> (s4 (f2 (comp A0 (g3 (comp B1 b07 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (i = 1) -> (t5 (g3 b07)) @ -j ])) [ (i = 0) -> (s4 b07) @ j, (i = 1) -> (s4 (f2 (g3 b07))) @ j ] ])) [ (j = 1) -> (t5 (g3 b07)) @ i ]))) @ i ] ], (k = 1) -> comp B1 (comp B1 b18 [ (i = 0)(j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ]) [ (i = 0) -> comp B1 (f2 (comp A0 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> (t5 (g3 b18)) @ (k /\ i) ]) [ (j = 1) -> (t5 (g3 b18)) @ (k /\ -i), (k = 1) -> (t5 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> (t5 (g3 b18)) @ i ])) @ -i ])) [ (j = 1) -> (s4 (f2 (g3 b18))) @ i, (k = 0) -> (s4 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) @ i, (k = 1) -> (s4 (f2 (comp A0 (g3 (comp B1 b18 [ (j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (i = 1) -> (t5 (g3 b18)) @ -j ])) [ (i = 0) -> (s4 b18) @ j, (i = 1) -> (s4 (f2 (g3 b18))) @ j ] ])) [ (j = 1) -> (t5 (g3 b18)) @ i ]))) @ i ] ] ]) [ (i = 0) -> comp B1 (f2 (g3 (q10 @ k))) [ (j = 0) -> comp B1 (f2 (g3 (q10 @ k))) [ (k = 0) -> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b07)) @ k ]), (k = 1) -> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b18)) @ k ]) ], (j = 1) -> f2 (comp A0 (g3 (q10 @ k)) [ (k = 0) -> comp A0 (g3 (comp B1 b07 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b07)) @ k ], (k = 1) -> comp A0 (g3 (comp B1 b18 [ (i = 1)(j = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1)(j = 1) -> (t5 (g3 b18)) @ k ] ]), (k = 0) -> f2 (comp A0 (g3 (comp B1 b07 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b07) [ (j = 1) -> (t5 (g3 b07)) @ -i ])) [ (j = 0) -> (s4 b07) @ i, (j = 1) -> (s4 (f2 (g3 b07))) @ i ] ])) [ (i = 1) -> (t5 (g3 b07)) @ j ]), (k = 1) -> f2 (comp A0 (g3 (comp B1 b18 [ (i = 1) -> comp B1 (f2 (comp A0 (g3 b18) [ (j = 1) -> (t5 (g3 b18)) @ -i ])) [ (j = 0) -> (s4 b18) @ i, (j = 1) -> (s4 (f2 (g3 b18))) @ i ] ])) [ (i = 1) -> (t5 (g3 b18)) @ j ]) ] ]) [ (k = 0) -> comp B1 b07 [ (i = 0)(j = 0) -> comp B1 (f2 (comp A0 (g3 b07) [ (k = 1) -> (t5 (g3 b07)) @ -i ])) [ (k = 0) -> (s4 b07) @ i, (k = 1) -> (s4 (f2 (g3 b07))) @ i ] ], (k = 1) -> comp B1 b18 [ (i = 0)(j = 0) -> comp B1 (f2 (comp A0 (g3 b18) [ (k = 1) -> (t5 (g3 b18)) @ -i ])) [ (k = 0) -> (s4 b18) @ i, (k = 1) -> (s4 (f2 (g3 b18))) @ i ] ] ] ] +\(A : U) -> \(B : U) -> + \(f : A -> B) -> \(g : B -> A) -> + \(s : \(y : B) -> IdP ( B) (f (g y)) y) -> + \(t : \(x : A) -> IdP ( A) (g (f x)) x) -> + \(sA : \(a : A) -> \(b : A) -> \(a0 : IdP ( A) a b) -> \(b0 : IdP ( A) a b) -> IdP ( IdP ( A) a b) a0 b0) -> \(b0 : B) -> \(b1 : B) -> \(p : IdP ( B) b0 b1) -> \(q : IdP ( B) b0 b1) -> + comp B (comp B (f (sA (g b0) (g b1) ( comp A (g (p @ j)) [ (j = 0) -> comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ], (j = 1) -> comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ] ]) ( comp A (g (q @ j)) [ (j = 0) -> comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ], (j = 1) -> comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ] ]) @ j @ k)) [ (k = 0) -> comp B b0 [ (i = 0) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ], (k = 1) -> comp B b1 [ (i = 0) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ] ]) [ (j = 0) -> comp B (comp B (comp B (comp B (p @ k) [ (i = 0) -> comp B (f (comp A (g (p @ k)) [ (j = 1) -> t (g (p @ k)) @ -i ])) [ (j = 0) -> s (p @ k) @ i, (j = 1) -> s (f (g (p @ k))) @ i ] ]) [ (k = 0) -> comp B (comp B b0 [ (i = 0)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ (k /\ i) ]) [ (j = 1) -> t (g b0) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b0)) @ i, (k = 0) -> s (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ])) @ i ] ], (k = 1) -> comp B (comp B b1 [ (i = 0)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ (k /\ i) ]) [ (j = 1) -> t (g b1) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b1)) @ i, (k = 0) -> s (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ])) @ i ] ] ]) [ (i = 0) -> comp B (f (g (p @ k))) [ (j = 0) -> comp B (f (g (p @ k))) [ (k = 0) -> f (comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ]) ], (j = 1) -> f (comp A (g (p @ k)) [ (k = 0) -> comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ], (k = 1) -> comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ] ]), (k = 0) -> f (comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ]) ] ]) [ (k = 0) -> comp B b0 [ (i = 0)(j = 0) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ], (k = 1) -> comp B b1 [ (i = 0)(j = 0) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ] ], (j = 1) -> comp B (comp B (comp B (comp B (q @ k) [ (i = 0) -> comp B (f (comp A (g (q @ k)) [ (j = 1) -> t (g (q @ k)) @ -i ])) [ (j = 0) -> s (q @ k) @ i, (j = 1) -> s (f (g (q @ k))) @ i ] ]) [ (k = 0) -> comp B (comp B b0 [ (i = 0)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ (k /\ i) ]) [ (j = 1) -> t (g b0) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b0)) @ i, (k = 0) -> s (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ])) @ i ] ], (k = 1) -> comp B (comp B b1 [ (i = 0)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ (k /\ i) ]) [ (j = 1) -> t (g b1) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b1)) @ i, (k = 0) -> s (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ])) @ i ] ] ]) [ (i = 0) -> comp B (f (g (q @ k))) [ (j = 0) -> comp B (f (g (q @ k))) [ (k = 0) -> f (comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ]) ], (j = 1) -> f (comp A (g (q @ k)) [ (k = 0) -> comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ], (k = 1) -> comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ] ]), (k = 0) -> f (comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ]) ] ]) [ (k = 0) -> comp B b0 [ (i = 0)(j = 0) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ], (k = 1) -> comp B b1 [ (i = 0)(j = 0) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ] ] ] -}