From: Carlo Angiuli Date: Mon, 9 Apr 2018 19:11:27 +0000 (-0400) Subject: Clean up isoToEquiv proof with Anders. X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=bf8253f482917e390fe8b44ceaf308405afeefc6;p=cubicaltt.git Clean up isoToEquiv proof with Anders. --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index dc2f405..a8e4ba1 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -185,36 +185,29 @@ lemIso (A B : U) (f : A -> B) (g : B -> A) rem0 : Path A (g y) x0 = comp ( A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> g y ] + rem0fill : Square A (g y) (g (f x0)) (g y) x0 + ( g (p0 @ i)) rem0 ( g y) (t x0) = + fill ( A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> g y ] + rem1 : Path A (g y) x1 = comp ( A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> g y ] + rem1fill : Square A (g y) (g (f x1)) (g y) x1 + ( g (p1 @ i)) rem1 ( g y) (t x1) = + fill ( A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> g y ] + p : Path A x0 x1 = - comp ( A) (g y) [ (i = 0) -> rem0 - , (i = 1) -> rem1 ] - - fill0 : Square A (g y) (g (f x0)) (g y) x0 - ( g (p0 @ i)) rem0 ( g y) (t x0) = - comp ( A) (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k - , (i = 0) -> g y - , (j = 0) -> g (p0 @ i) ] - - fill1 : Square A (g y) (g (f x1)) (g y) x1 - ( g (p1 @ i)) rem1 ( g y) (t x1) = - comp ( A) (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k - , (i = 0) -> g y - , (j = 0) -> g (p1 @ i) ] - - fill2 : Square A (g y) (g y) x0 x1 + comp ( A) (g y) [ (i = 1) -> rem1, (i = 0) -> rem0 ] + + pfill : Square A (g y) (g y) x0 x1 ( g y) p rem0 rem1 = - comp ( A) (g y) [ (i = 0) -> rem0 @ j /\ k - , (i = 1) -> rem1 @ j /\ k - , (j = 0) -> g y ] + fill ( A) (g y) [ (i = 1) -> rem1, (i = 0) -> rem0 ] sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) ( g y) ( g (f (p @ i))) ( g (p0 @ j)) ( g (p1 @ j)) = - comp ( A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k - , (i = 1) -> fill1 @ j @ -k + comp ( A) (pfill @ i @ j) [ (i = 0) -> rem0fill @ j @ -k + , (i = 1) -> rem1fill @ j @ -k , (j = 0) -> g y , (j = 1) -> t (p @ i) @ -k ]