From: Anders Mörtberg Date: Tue, 5 Jan 2016 09:21:54 +0000 (+0100) Subject: remove all <_> X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9b57f22b8869e985305c197e541c293010b43a46;p=cubicaltt.git remove all <_> --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index c617191..6105336 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -87,7 +87,7 @@ transIdFun (A B : U) (w : equiv A B) u : A = comp (A) a [] q : Id B (w.1 u) b = w.1 (comp (A) a [(i=1) -> a]) in comp ( B) - (comp ( B) (comp ( B) (comp ( B) (w.1 u) [(i=0)->q]) [(i=0)-><_>b]) [(i=0)-><_>b]) [(i=0)-><_>b] + (comp ( B) (comp ( B) (comp ( B) (w.1 u) [(i=0)->q]) [(i=0)->b]) [(i=0)->b]) [(i=0)->b] idToId (A B : U) (w : equiv A B) : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w @@ -104,44 +104,44 @@ lemIso (A B : U) (f : A -> B) (g : B -> A) Id (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) where rem0 : Id A (g y) x0 = - comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ] + comp ( A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> g y ] rem1 : Id A (g y) x1 = - comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ] + comp ( A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> g y ] p : Id A x0 x1 = - comp (<_> A) (g y) [ (i = 0) -> rem0 + 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) ] + 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) ] + 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 - (<_> g y) p rem0 rem1 = - comp (<_> A) (g y) [ (i = 0) -> rem0 @ j /\ k + ( g y) p rem0 rem1 = + comp ( A) (g y) [ (i = 0) -> rem0 @ j /\ k , (i = 1) -> rem1 @ j /\ k - , (j = 0) -> <_> g y ] + , (j = 0) -> g y ] 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 + comp ( A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k , (i = 1) -> fill1 @ j @ -k - , (j = 0) -> <_> g y + , (j = 0) -> g y , (j = 1) -> t (p @ i) @ -k ] sq1 : Square B y y (f x0) (f x1) - (<_>y) ( f (p @ i)) p0 p1 = - comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) + (y) ( f (p @ i)) p0 p1 = + comp ( B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) , (i = 1) -> s (p1 @ j) , (j = 1) -> s (f (p @ i)) , (j = 0) -> s y ] diff --git a/examples/prelude.ctt b/examples/prelude.ctt index f452fb2..856790e 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -27,7 +27,7 @@ subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = substEq (A : U) (P : A -> U) (a : A) (e : P a) : Id (P a) e (subst A P a a (refl A a) e) = - fill (<_> P a) e [] + fill ( P a) e [] substInv (A : U) (P : A -> U) (a b : A) (p : Id A a b) : P b -> P a = subst A P b a ( p @ -i) @@ -51,7 +51,7 @@ JEq (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) inv (A : U) (a b : A) (p : Id A a b) : Id A b a = p @ -i compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = - comp (<_>A) (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ] + comp (A) (p @ i) [ (i = 1) -> q, (i=0) -> a ] compId' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = subst A (Id A a) b c q p @@ -62,7 +62,7 @@ compId'' (A : U) (a b : A) (p : Id A a b) : (c : A) -> (q : Id A b c) -> Id A a compUp (A : U) (a a' b b' : A) (p : Id A a a') (q : Id A b b') (r : Id A a b) : Id A a' b' = - comp (<_>A) (r @ i) [(i = 0) -> p, (i = 1) -> q] + comp (A) (r @ i) [(i = 0) -> p, (i = 1) -> q] compDown (A : U) (a a' b b' : A) (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b = @@ -70,17 +70,17 @@ compDown (A : U) (a a' b b' : A) lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p = - comp (<_>A) - ((fill (<_>A) (p @ i) [(i=0) -> <_>a, (i=1) -> q]) @ -j) - [ (i=0) -> <_> a + comp (A) + ((fill (A) (p @ i) [(i=0) -> a, (i=1) -> q]) @ -j) + [ (i=0) -> a , (i=1) -> q @ - (j \/ k) - , (j=0) -> fill (<_>A) ((compId A a b c p q @ i)) - [(i=0) -> <_>a, (i=1) -> q @ -k ] - , (j=1) -> <_> p @ i + , (j=0) -> fill (A) ((compId A a b c p q @ i)) + [(i=0) -> a, (i=1) -> q @ -k ] + , (j=1) -> p @ i ] lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) = - comp (<_>A) (p @ (-i \/ j)) [(i=0) -> b, (j=1) -> b, (i=1) -> p @ (j \/ k)] + comp (A) (p @ (-i \/ j)) [(i=0) -> b, (j=1) -> b, (i=1) -> p @ (j \/ k)] test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0) test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) @@ -90,17 +90,17 @@ test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c) (r : Id A b d) : Id A c d = - comp (<_>A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] + comp (A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' = - comp (<_> A) a - [ (j = 0) -> comp (<_> A) (p @ i) + comp ( A) a + [ (j = 0) -> comp ( A) (p @ i) [ (k = 0) -> p @ i , (i = 0) -> a , (i = 1) -> q @ k /\ l] - , (j = 1) -> comp (<_> A) (p @ i) + , (j = 1) -> comp ( A) (p @ i) [ (k = 0) -> p @ i , (i = 0) -> a , (i = 1) -> q' @ k /\ l] @@ -108,8 +108,8 @@ lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) , (k = 1) -> s @ j ] IdPathTest1 (A : U) (a b : A) (p : Id A a b) : - Id (Id A a b) p ( comp (<_> A) (p @ i) [(i=0) -> <_> a,(i=1) -> <_> b]) = - fill (<_> A) (p @ i) [(i=0) -> <_> a,(i=1) -> <_> b] @ j + Id (Id A a b) p ( comp ( A) (p @ i) [(i=0) -> a,(i=1) -> b]) = + fill ( A) (p @ i) [(i=0) -> a,(i=1) -> b] @ j idfun (A : U) (a : A) : A = a @@ -127,7 +127,7 @@ Square (A : U) (a0 a1 b0 b1 : A) = IdP ( (IdP ( A) (u @ i) (v @ i))) r0 r1 constSquare (A : U) (a : A) (p : Id A a a) : Square A a a a a p p p p = - comp (<_>A) a + comp (A) a [(i = 0) -> p @ (j \/ - k), (i = 1) -> p @ (j /\ k), (j = 0) -> p @ (i \/ - k), @@ -138,7 +138,7 @@ set (A : U) : U = (a b : A) -> prop (Id A a b) groupoid (A : U) : U = (a b : A) -> set (Id A a b) propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q = - comp (<_>A) a [ (i=0) -> h a a + comp (A) a [ (i=0) -> h a a , (i=1) -> h a b , (j=0) -> h a (p @ i) , (j=1) -> h a (q @ i)] diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 693c628..58c6920 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -6,7 +6,7 @@ module univalence where import equiv -import bool +-- import bool ------------------------------------------------------------------------------ -- Proof of univalence using unglue: @@ -96,24 +96,24 @@ lem1 (B:U) : isContr ((X:U) * equiv X B) = ,unglueElemB ,\(b : B) -> let center : fiber glueB B unglueElemB b - = (glueElem (comp (<_> B) b [(i=0) -> <_> b + = (glueElem (comp ( B) b [(i=0) -> b ,(i=1) -> (w.2.2 b).1.2]) [(i=0) -> b ,(i=1) -> (w.2.2 b).1.1] - ,fill (<_> B) b [(i=0) -> <_> b + ,fill ( B) b [(i=0) -> b ,(i=1) -> (w.2.2 b).1.2]) contr (v : fiber glueB B unglueElemB b) : Id (fiber glueB B unglueElemB b) center v - = (glueElem (comp (<_> B) b [(i=0) -> v.2 @ (j /\ k) + = (glueElem (comp ( B) b [(i=0) -> v.2 @ (j /\ k) ,(i=1) -> ((w.2.2 b).2 v @ j).2 - ,(j=0) -> fill (<_> B) b [(i=0) -> <_> b + ,(j=0) -> fill ( B) b [(i=0) -> b ,(i=1) -> (w.2.2 b).1.2] ,(j=1) -> v.2]) [(i=0) -> v.2 @ j ,(i=1) -> ((w.2.2 b).2 v @ j).1] - ,fill (<_> B) b [(i=0) -> v.2 @ (j /\ l) + ,fill ( B) b [(i=0) -> v.2 @ (j /\ l) ,(i=1) -> ((w.2.2 b).2 v @ j).2 - ,(j=0) -> fill (<_> B) b [(i=0) -> <_> b + ,(j=0) -> fill ( B) b [(i=0) -> b ,(i=1) -> (w.2.2 b).1.2] ,(j=1) -> v.2]) in (center,contr))) @@ -144,100 +144,100 @@ corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (transEquiv' B A,univalence B A) --- Some tests of normal forms: -testUniv1 (A : U) : Id U A A = - trans (equiv A A) (Id U A A) ( corrUniv A A @ -i) (idEquiv A) +-- -- Some tests of normal forms: +-- testUniv1 (A : U) : Id U A A = +-- trans (equiv A A) (Id U A A) ( corrUniv A A @ -i) (idEquiv A) --- obtained by normal form -ntestUniv1 (A:U) : Id U A A = - comp (<_>U) - (comp (<_>U) A - [ (i = 0) -> comp (<_>U) A [ (l = 0) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> - ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ], (l = 1) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> - ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> A ]) [ (i = 0) -> A, (i = 1) -> A ] +-- -- obtained by normal form +-- ntestUniv1 (A:U) : Id U A A = +-- comp (<_>U) +-- (comp (<_>U) A +-- [ (i = 0) -> comp (<_>U) A [ (l = 0) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> +-- ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ], (l = 1) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> +-- ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> A ]) [ (i = 0) -> A, (i = 1) -> A ] -testUniv2 : bool = trans bool bool (ntestUniv1 bool) true +-- testUniv2 : bool = trans bool bool (ntestUniv1 bool) true -ntestUniv2 : bool = - comp ( comp (<_>U) (comp (<_>U) bool [ (i = 0) -> comp (<_>U) bool [ (j = 0) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> - ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ], (j = 1) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> - ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] +-- ntestUniv2 : bool = +-- comp ( comp (<_>U) (comp (<_>U) bool [ (i = 0) -> comp (<_>U) bool [ (j = 0) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> +-- ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ], (j = 1) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> +-- ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] --- A small test of univalence using boolean negation -isEquivNegBool : isEquiv bool bool negBool = - gradLemma bool bool negBool negBool negBoolK negBoolK +-- -- A small test of univalence using boolean negation +-- isEquivNegBool : isEquiv bool bool negBool = +-- gradLemma bool bool negBool negBool negBoolK negBoolK -eqBool : Id U bool bool = - trans (equiv bool bool) (Id U bool bool) - ( corrUniv bool bool @ -i) (negBool,isEquivNegBool) +-- eqBool : Id U bool bool = +-- trans (equiv bool bool) (Id U bool bool) +-- ( corrUniv bool bool @ -i) (negBool,isEquivNegBool) -test1 : bool = trans bool bool eqBool true -test2 : bool = trans bool bool eqBool false +-- test1 : bool = trans bool bool eqBool true +-- test2 : bool = trans bool bool eqBool false ------------------------------------------------------------------------------- --- The direct proof of univalence using transEquiv which is too slow --- to normalize: +-- ------------------------------------------------------------------------------ +-- -- The direct proof of univalence using transEquiv which is too slow +-- -- to normalize: --- transEquiv is an equiv -transEquivIsEquiv (A B : U) - : isEquiv (Id U A B) (equiv A B) (transEquiv A B) - = gradLemma (Id U A B) (equiv A B) (transEquiv A B) - (transEquivToId A B) (idToId A B) (eqToEq A B) +-- -- transEquiv is an equiv +-- transEquivIsEquiv (A B : U) +-- : isEquiv (Id U A B) (equiv A B) (transEquiv A B) +-- = gradLemma (Id U A B) (equiv A B) (transEquiv A B) +-- (transEquivToId A B) (idToId A B) (eqToEq A B) --- Univalence proved using transEquiv -univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = - isoId (Id U A B) (equiv A B) (transEquiv A B) - (transEquivToId A B) (idToId A B) (eqToEq A B) +-- -- Univalence proved using transEquiv +-- univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = +-- isoId (Id U A B) (equiv A B) (transEquiv A B) +-- (transEquivToId A B) (idToId A B) (eqToEq A B) -univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) = - (transEquiv A B,transEquivIsEquiv A B) +-- univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) = +-- (transEquiv A B,transEquivIsEquiv A B) --- univalenceTrans takes extremely much memory when normalizing +-- -- univalenceTrans takes extremely much memory when normalizing --- This also takes too long to normalize: -slowtest (A : U) : Id (equiv A A) - (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) = - idToId A A (idEquiv A) +-- -- This also takes too long to normalize: +-- slowtest (A : U) : Id (equiv A A) +-- (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) = +-- idToId A A (idEquiv A) ------------------------------------------------------------------------------- --- TODO: Adapt this to new definition of equiv - --- The canonical map defined using J --- canIdToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B = --- J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A) - --- canDiagTrans (A : U) : Id (A -> A) (canIdToEquiv A A (<_> A)).1 (idfun A) = --- fill (<_> A -> A) (idfun A) [] @ -i - --- transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) = --- \ (a : A) -> fill (<_> A) a [] @ i - --- canIdToEquivLem (A : U) : (B : U) (p : Id U A B) -> --- Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1 --- = J U A --- (\ (B : U) (p : Id U A B) -> --- Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1) --- (compId (A -> A) --- (canIdToEquiv A A (<_> A)).1 (idfun A) (trans A A (<_> A)) --- (canDiagTrans A) (transDiagTrans A)) - --- canIdToEquivIsTransEquiv (A B : U) : --- Id (Id U A B -> equiv A B) (canIdToEquiv A B) (transEquiv A B) = --- \ (p : Id U A B) -> --- equivLemma A B (canIdToEquiv A B p) (transEquiv A B p) --- (canIdToEquivLem A B p) @ i - --- -- The canonical map is an equivalence --- univalenceJ (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) = --- substInv (Id U A B -> equiv A B) --- (isEquiv (Id U A B) (equiv A B)) --- (canIdToEquiv A B) (transEquiv A B) --- (canIdToEquivIsTransEquiv A B) --- (transEquivIsEquiv A B) \ No newline at end of file +-- ------------------------------------------------------------------------------ +-- -- TODO: Adapt this to new definition of equiv + +-- -- The canonical map defined using J +-- -- canIdToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B = +-- -- J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A) + +-- -- canDiagTrans (A : U) : Id (A -> A) (canIdToEquiv A A (<_> A)).1 (idfun A) = +-- -- fill (<_> A -> A) (idfun A) [] @ -i + +-- -- transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) = +-- -- \ (a : A) -> fill (<_> A) a [] @ i + +-- -- canIdToEquivLem (A : U) : (B : U) (p : Id U A B) -> +-- -- Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1 +-- -- = J U A +-- -- (\ (B : U) (p : Id U A B) -> +-- -- Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1) +-- -- (compId (A -> A) +-- -- (canIdToEquiv A A (<_> A)).1 (idfun A) (trans A A (<_> A)) +-- -- (canDiagTrans A) (transDiagTrans A)) + +-- -- canIdToEquivIsTransEquiv (A B : U) : +-- -- Id (Id U A B -> equiv A B) (canIdToEquiv A B) (transEquiv A B) = +-- -- \ (p : Id U A B) -> +-- -- equivLemma A B (canIdToEquiv A B p) (transEquiv A B p) +-- -- (canIdToEquivLem A B p) @ i + +-- -- -- The canonical map is an equivalence +-- -- univalenceJ (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) = +-- -- substInv (Id U A B -> equiv A B) +-- -- (isEquiv (Id U A B) (equiv A B)) +-- -- (canIdToEquiv A B) (transEquiv A B) +-- -- (canIdToEquivIsTransEquiv A B) +-- -- (transEquivIsEquiv A B) \ No newline at end of file