if A and B are isomorphic, set A -> set B, normal form

diff --git a/examples/prop.ctt b/examples/prop.ctt
index 148af5b594fbc883cb613d8b177af15b42605b46..fe6cf7ca4934ecd04fe664e5bfc2f52f6663d174 100644 (file)
--- a/examples/prop.ctt
+++ b/examples/prop.ctt
@@ -24,3 +24,18 @@ lemProp (A B : U) (f : A -> B) (g : B -> A)
                                ] 
   ]
 -}
+
+lemSet (A B : U) (f : A -> B) (g : B -> A)
+      (s : (y:B) -> Id B (f (g y)) y)
+      (t : (x:A) -> Id A (g (f x)) x) (sA:set A) : set B =
+ \ (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 ] ] ] ] 
+-}