Improve printing of lambdas and paths

diff --git a/CTT.hs b/CTT.hs
index b9dfb0b304073cdecfc31efe9196bf05272dd2ed..27be0be258d8f9c92b250f7c3e622102d608f850 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -382,19 +382,18 @@ showVal v = case v of
                        <+> (hsep $ map ((char '@' <+>) . showFormula) phis)
   VPi a l@(VLam x t b)
     | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
-    | otherwise -> parens (text x <+> colon <+> showVal t) <+> text "->" <+> showVal b
+    | otherwise          -> char '(' <> showLam v
   VPi a b           -> text "Pi" <+> showVals [a,b]
   VPair u v         -> parens (showVal u <> comma <> showVal v)
   VSigma u v        -> text "Sigma" <+> showVals [u,v]
   VApp u v          -> showVal u <+> showVal1 v
-  VLam x t e        -> char '\\' <> parens (text x <+> colon <+> showVal t) <+>
-                         text "->" <+> showVal e
+  VLam{}            -> text "\\(" <> showLam v
+  VPath{}           -> char '<' <> showPath v
   VSplit u v        -> showVal u <+> showVal1 v
   VVar x _          -> text x
   VFst u            -> showVal1 u <> text ".1"
   VSnd u            -> showVal1 u <> text ".2"
   VIdP v0 v1 v2     -> text "IdP" <+> showVals [v0,v1,v2]
-  VPath i v         -> char '<' <> text (show i) <> char '>' <+> showVal v
   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]
@@ -405,6 +404,27 @@ showVal v = case v of
   VElimComp a es t    -> text "elimComp" <+> showVal1 a <+> text (showSystem es)
                          <+> showVal1 t
 
+showPath :: Val -> Doc
+showPath e = case e of
+  VPath i a@VPath{} -> text (show i) <+> showPath a
+  VPath i a         -> text (show i) <> char '>' <+> showVal a
+  _                 -> showVal e
+
+-- Merge lambdas of the same type
+showLam :: Val -> Doc
+showLam e = case e of
+  VLam x t a@(VLam _ t' _)
+    | t == t'   -> text x <+> showLam a
+    | otherwise -> text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a
+  VPi _ (VLam x t a@(VPi _ (VLam _ t' _)))
+    | t == t'   -> text x <+> showLam a
+    | otherwise -> text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a
+  VLam x t e         ->
+    text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal e
+  VPi _ (VLam x t e) ->
+    text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal e
+  _ -> showVal e
+
 showVal1 :: Val -> Doc
 showVal1 v = case v of
   VU                -> showVal v
@@ -416,3 +436,4 @@ showVal1 v = case v of
 
 showVals :: [Val] -> Doc
 showVals = hsep . map showVal1
+

diff --git a/examples/prop.ctt b/examples/prop.ctt
index cb6d02cdcec5593a646bdc1ef4c2c9253c54a7bb..f9af4ede5c90d0c7b61420c6de0b1ee13d6a6ca7 100644 (file)
--- a/examples/prop.ctt
+++ b/examples/prop.ctt
@@ -8,19 +8,28 @@ 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
-\(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 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 ] ]
-  ]
+
+\(A B : U) -> \(f : A -> B) -> \(g : B -> A) ->
+ \(s : (y : B) -> IdP (<!0> B) (f (g y)) y) ->
+ \(t : (x : A) -> IdP (<!0> A) (g (f x)) x) ->
+ \(pA : (a : A) -> (b : A) -> IdP (<!0> A) a b) ->
+  \(b0 b1 : B) ->
+  <!1> comp B (f (pA (g b0) (g b1) @ !1))
+    [ (!1 = 0) -> <!2> comp B b0
+                   [ (!2 = 0) -> <!3> comp B (f (comp A (g b0)
+                                              [ (!3 = 1) -> <!4> t (g b0) @ -!4 ]))
+                                              [ (!3 = 0) -> <!4> s b0 @ !4, (!3 = 1) -> <!4> s (f (g b0)) @ !4 ]
+                   ]
+    , (!1 = 1) -> <!2> comp B b1 [ (!2 = 0) -> <!3> comp B (f (comp A (g b1) [ (!3 = 1) -> <!4> t (g b1) @ -!4 ]))
+                                                     [ (!3 = 0) -> <!4> s b1 @ !4, (!3 = 1) -> <!4> s (f (g b1)) @ !4 ] ] ]
+
+\(A B : U) -> \(f : A -> B) -> \(g : B -> A) ->
+  \(s : (y : B) -> IdP (<!0> B) (f (g y)) y) ->
+  \(t : (x : A) -> IdP (<!0> A) (g (f x)) x) ->
+  \(pA : (a b : A) -> IdP (<!0> A) a b) ->
+  \(b0 b1 : B) ->
+  <!1> comp B (f (pA (g b0) (g b1) @ !1)) [ (!1 = 0) -> <!2> comp B b0 [ (!2 = 0) -> <!3> comp B (f (comp A (g b0) [ (!3 = 1) -> <!4> t (g b0) @ -!4 ])) [ (!3 = 0) -> <!4> s b0 @ !4, (!3 = 1) -> <!4> s (f (g b0)) @ !4 ] ], (!1 = 1) -> <!2> comp B b1 [ (!2 = 0) -> <!3> comp B (f (comp A (g b1) [ (!3 = 1) -> <!4> t (g b1) @ -!4 ])) [ (!3 = 0) -> <!4> s b1 @ !4, (!3 = 1) -> <!4> s (f (g b1)) @ !4 ] ] ]
+
 -}
 
 lemSet (A B : U) (f : A -> B) (g : B -> A)
@@ -29,10 +38,13 @@ 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
-\(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 ] ] ] ]
+
+\(A B : U) -> \(f : A -> B) -> \(g : B -> A) ->
+  \(s : (y : B) -> IdP (<!0> B) (f (g y)) y) ->
+  \(t : (x : A) -> IdP (<!0> A) (g (f x)) x) ->
+  \(sA : (a b : A) -> (a0 b0 : IdP (<!0> A) a b) -> IdP (<!0> IdP (<!0> A) a b) a0 b0) ->
+  \(b0 b1 : B) ->
+  \(p q : IdP (<!0> B) b0 b1) ->
+  <!1 !2> comp B (comp B (f (sA (g b0) (g b1) (<!1> comp A (g (p @ !1)) [ (!1 = 0) -> <!2> comp A (g (comp B b0 [ (!2 = 1) -> <!3> comp B (f (comp A (g b0) [ (!3 = 1) -> <!4> t (g b0) @ -!4 ])) [ (!3 = 0) -> <!4> s b0 @ !4, (!3 = 1) -> <!4> s (f (g b0)) @ !4 ] ])) [ (!2 = 1) -> <!3> t (g b0) @ !3 ], (!1 = 1) -> <!2> comp A (g (comp B b1 [ (!2 = 1) -> <!3> comp B (f (comp A (g b1) [ (!3 = 1) -> <!4> t (g b1) @ -!4 ])) [ (!3 = 0) -> <!4> s b1 @ !4, (!3 = 1) -> <!4> s (f (g b1)) @ !4 ] ])) [ (!2 = 1) -> <!3> t (g b1) @ !3 ] ]) (<!1> comp A (g (q @ !1)) [ (!1 = 0) -> <!2> comp A (g (comp B b0 [ (!2 = 1) -> <!3> comp B (f (comp A (g b0) [ (!3 = 1) -> <!4> t (g b0) @ -!4 ])) [ (!3 = 0) -> <!4> s b0 @ !4, (!3 = 1) -> <!4> s (f (g b0)) @ !4 ] ])) [ (!2 = 1) -> <!3> t (g b0) @ !3 ], (!1 = 1) -> <!2> comp A (g (comp B b1 [ (!2 = 1) -> <!3> comp B (f (comp A (g b1) [ (!3 = 1) -> <!4> t (g b1) @ -!4 ])) [ (!3 = 0) -> <!4> s b1 @ !4, (!3 = 1) -> <!4> s (f (g b1)) @ !4 ] ])) [ (!2 = 1) -> <!3> t (g b1) @ !3 ] ]) @ !1 @ !2)) [ (!2 = 0) -> <!3> comp B b0 [ (!3 = 0) -> <!4> comp B (f (comp A (g b0) [ (!4 = 1) -> <!5> t (g b0) @ -!5 ])) [ (!4 = 0) -> <!5> s b0 @ !5, (!4 = 1) -> <!5> s (f (g b0)) @ !5 ] ], (!2 = 1) -> <!3> comp B b1 [ (!3 = 0) -> <!4> comp B (f (comp A (g b1) [ (!4 = 1) -> <!5> t (g b1) @ -!5 ])) [ (!4 = 0) -> <!5> s b1 @ !5, (!4 = 1) -> <!5> s (f (g b1)) @ !5 ] ] ]) [ (!1 = 0) -> <!3> comp B (comp B (comp B (comp B (p @ !2) [ (!3 = 0) -> <!4> comp B (f (comp A (g (p @ !2)) [ (!4 = 1) -> <!5> t (g (p @ !2)) @ -!5 ])) [ (!4 = 0) -> <!5> s (p @ !2) @ !5, (!4 = 1) -> <!5> s (f (g (p @ !2))) @ !5 ] ]) [ (!2 = 0) -> <!4> comp B (comp B b0 [ (!3 = 0)(!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ]) [ (!3 = 0) -> <!5> comp B (f (comp A (comp A (g (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> <!6> t (g b0) @ (!5 /\ !6) ]) [ (!4 = 1) -> <!6> t (g b0) @ (!5 /\ -!6), (!5 = 1) -> <!6> t (comp A (g (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b0) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> <!6> s (f (g b0)) @ !6, (!5 = 0) -> <!6> s (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ]) @ !6, (!5 = 1) -> <!6> s (f (comp A (g (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b0) @ !5 ])) @ !6 ] ], (!2 = 1) -> <!4> comp B (comp B b1 [ (!3 = 0)(!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ]) [ (!3 = 0) -> <!5> comp B (f (comp A (comp A (g (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> <!6> t (g b1) @ (!5 /\ !6) ]) [ (!4 = 1) -> <!6> t (g b1) @ (!5 /\ -!6), (!5 = 1) -> <!6> t (comp A (g (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b1) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> <!6> s (f (g b1)) @ !6, (!5 = 0) -> <!6> s (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ]) @ !6, (!5 = 1) -> <!6> s (f (comp A (g (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b1) @ !5 ])) @ !6 ] ] ]) [ (!3 = 0) -> <!4> comp B (f (g (p @ !2))) [ (!2 = 0) -> <!5> f (comp A (g (comp B b0 [ (!5 = 1) -> <!6> comp B (f (comp A (g b0) [ (!6 = 1) -> <!7> t (g b0) @ -!7 ])) [ (!6 = 0) -> <!7> s b0 @ !7, (!6 = 1) -> <!7> s (f (g b0)) @ !7 ] ])) [ (!5 = 1) -> <!6> t (g b0) @ !6 ]), (!2 = 1) -> <!5> f (comp A (g (comp B b1 [ (!5 = 1) -> <!6> comp B (f (comp A (g b1) [ (!6 = 1) -> <!7> t (g b1) @ -!7 ])) [ (!6 = 0) -> <!7> s b1 @ !7, (!6 = 1) -> <!7> s (f (g b1)) @ !7 ] ])) [ (!5 = 1) -> <!6> t (g b1) @ !6 ]), (!4 = 0) -> <!5> comp B (f (g (p @ !2))) [ (!2 = 0) -> <!6> f (comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b0) [ (!7 = 1) -> <!8> t (g b0) @ -!8 ])) [ (!7 = 0) -> <!8> s b0 @ !8, (!7 = 1) -> <!8> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b0) @ !7 ]), (!2 = 1) -> <!6> f (comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b1) [ (!7 = 1) -> <!8> t (g b1) @ -!8 ])) [ (!7 = 0) -> <!8> s b1 @ !8, (!7 = 1) -> <!8> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b1) @ !7 ]) ], (!4 = 1) -> <!5> f (comp A (g (p @ !2)) [ (!2 = 0) -> <!6> comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b0) [ (!7 = 1) -> <!8> t (g b0) @ -!8 ])) [ (!7 = 0) -> <!8> s b0 @ !8, (!7 = 1) -> <!8> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b0) @ !7 ], (!2 = 1) -> <!6> comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b1) [ (!7 = 1) -> <!8> t (g b1) @ -!8 ])) [ (!7 = 0) -> <!8> s b1 @ !8, (!7 = 1) -> <!8> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b1) @ !7 ] ]) ] ]) [ (!2 = 0) -> <!4> comp B b0 [ (!3 = 0)(!4 = 0) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ], (!2 = 1) -> <!4> comp B b1 [ (!3 = 0)(!4 = 0) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ] ], (!1 = 1) -> <!3> comp B (comp B (comp B (comp B (q @ !2) [ (!3 = 0) -> <!4> comp B (f (comp A (g (q @ !2)) [ (!4 = 1) -> <!5> t (g (q @ !2)) @ -!5 ])) [ (!4 = 0) -> <!5> s (q @ !2) @ !5, (!4 = 1) -> <!5> s (f (g (q @ !2))) @ !5 ] ]) [ (!2 = 0) -> <!4> comp B (comp B b0 [ (!3 = 0)(!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ]) [ (!3 = 0) -> <!5> comp B (f (comp A (comp A (g (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> <!6> t (g b0) @ (!5 /\ !6) ]) [ (!4 = 1) -> <!6> t (g b0) @ (!5 /\ -!6), (!5 = 1) -> <!6> t (comp A (g (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b0) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> <!6> s (f (g b0)) @ !6, (!5 = 0) -> <!6> s (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ]) @ !6, (!5 = 1) -> <!6> s (f (comp A (g (comp B b0 [ (!4 = 1) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b0) @ !5 ])) @ !6 ] ], (!2 = 1) -> <!4> comp B (comp B b1 [ (!3 = 0)(!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ]) [ (!3 = 0) -> <!5> comp B (f (comp A (comp A (g (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> <!6> t (g b1) @ (!5 /\ !6) ]) [ (!4 = 1) -> <!6> t (g b1) @ (!5 /\ -!6), (!5 = 1) -> <!6> t (comp A (g (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b1) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> <!6> s (f (g b1)) @ !6, (!5 = 0) -> <!6> s (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ]) @ !6, (!5 = 1) -> <!6> s (f (comp A (g (comp B b1 [ (!4 = 1) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> <!5> t (g b1) @ !5 ])) @ !6 ] ] ]) [ (!3 = 0) -> <!4> comp B (f (g (q @ !2))) [ (!2 = 0) -> <!5> f (comp A (g (comp B b0 [ (!5 = 1) -> <!6> comp B (f (comp A (g b0) [ (!6 = 1) -> <!7> t (g b0) @ -!7 ])) [ (!6 = 0) -> <!7> s b0 @ !7, (!6 = 1) -> <!7> s (f (g b0)) @ !7 ] ])) [ (!5 = 1) -> <!6> t (g b0) @ !6 ]), (!2 = 1) -> <!5> f (comp A (g (comp B b1 [ (!5 = 1) -> <!6> comp B (f (comp A (g b1) [ (!6 = 1) -> <!7> t (g b1) @ -!7 ])) [ (!6 = 0) -> <!7> s b1 @ !7, (!6 = 1) -> <!7> s (f (g b1)) @ !7 ] ])) [ (!5 = 1) -> <!6> t (g b1) @ !6 ]), (!4 = 0) -> <!5> comp B (f (g (q @ !2))) [ (!2 = 0) -> <!6> f (comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b0) [ (!7 = 1) -> <!8> t (g b0) @ -!8 ])) [ (!7 = 0) -> <!8> s b0 @ !8, (!7 = 1) -> <!8> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b0) @ !7 ]), (!2 = 1) -> <!6> f (comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b1) [ (!7 = 1) -> <!8> t (g b1) @ -!8 ])) [ (!7 = 0) -> <!8> s b1 @ !8, (!7 = 1) -> <!8> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b1) @ !7 ]) ], (!4 = 1) -> <!5> f (comp A (g (q @ !2)) [ (!2 = 0) -> <!6> comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b0) [ (!7 = 1) -> <!8> t (g b0) @ -!8 ])) [ (!7 = 0) -> <!8> s b0 @ !8, (!7 = 1) -> <!8> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b0) @ !7 ], (!2 = 1) -> <!6> comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> <!7> comp B (f (comp A (g b1) [ (!7 = 1) -> <!8> t (g b1) @ -!8 ])) [ (!7 = 0) -> <!8> s b1 @ !8, (!7 = 1) -> <!8> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> <!7> t (g b1) @ !7 ] ]) ] ]) [ (!2 = 0) -> <!4> comp B b0 [ (!3 = 0)(!4 = 0) -> <!5> comp B (f (comp A (g b0) [ (!5 = 1) -> <!6> t (g b0) @ -!6 ])) [ (!5 = 0) -> <!6> s b0 @ !6, (!5 = 1) -> <!6> s (f (g b0)) @ !6 ] ], (!2 = 1) -> <!4> comp B b1 [ (!3 = 0)(!4 = 0) -> <!5> comp B (f (comp A (g b1) [ (!5 = 1) -> <!6> t (g b1) @ -!6 ])) [ (!5 = 0) -> <!6> s b1 @ !6, (!5 = 1) -> <!6> s (f (g b1)) @ !6 ] ] ] ]
+
 -}