From 26a03d760275690cac1e79451f892a7e36e68eb7 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 7 Jul 2016 16:03:02 +0200 Subject: [PATCH] rename glue -> Glue, glueElem -> glue and unglueElem -> unglue --- Exp.cf | 6 +++--- examples/aim.ctt | 4 ++-- examples/bool.ctt | 10 +++++----- examples/demo.ctt | 2 +- examples/equiv.ctt | 8 ++++---- examples/univalence.ctt | 24 ++++++++++++------------ 6 files changed, 27 insertions(+), 27 deletions(-) diff --git a/Exp.cf b/Exp.cf index 5296aeb..bd013b9 100644 --- a/Exp.cf +++ b/Exp.cf @@ -39,9 +39,9 @@ PathP. Exp3 ::= "PathP" Exp4 Exp4 Exp4 ; Comp. Exp3 ::= "comp" Exp4 Exp4 System ; Trans. Exp3 ::= "transport" Exp4 Exp4 ; Fill. Exp3 ::= "fill" Exp4 Exp4 System ; -Glue. Exp3 ::= "glue" Exp4 System ; -GlueElem. Exp3 ::= "glueElem" Exp4 System ; -UnGlueElem. Exp3 ::= "unglueElem" Exp4 System ; +Glue. Exp3 ::= "Glue" Exp4 System ; +GlueElem. Exp3 ::= "glue" Exp4 System ; +UnGlueElem. Exp3 ::= "unglue" Exp4 System ; Fst. Exp4 ::= Exp4 ".1" ; Snd. Exp4 ::= Exp4 ".2" ; Pair. Exp5 ::= "(" Exp "," [Exp] ")" ; diff --git a/examples/aim.ctt b/examples/aim.ctt index 4ec7ca1..d308cee 100644 --- a/examples/aim.ctt +++ b/examples/aim.ctt @@ -552,7 +552,7 @@ gradLemma (A B : U) (f : A -> B) (g : B -> A) isoPath (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) : Path U A B = - glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) + Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) , (i = 1) -> (B,idfun B,idIsEquiv B) ] @@ -648,7 +648,7 @@ testNOneZ : Z = transport ( sucPathZ @ - i) zeroZ ----------------------------------------------------------------- --- Using glue we get a proof of univalence, see univalence.ctt -- +-- Using Glue we get a proof of univalence, see univalence.ctt -- diff --git a/examples/bool.ctt b/examples/bool.ctt index eb159f9..485c0b5 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -116,7 +116,7 @@ negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 negBool -- lemTest (A : U) : (B : U) (p : Path U A B) (a : A) -> PathP p a (transport p a) = -- J U A (\(B : U) (p : Path U A B) -> (a : A) -> PathP p a (transport p a)) (refl A) --- test : PathP boolEqF2 true oneF2 = glueElem oneF2 [ (i = 0) -> true ] +-- test : PathP boolEqF2 true oneF2 = glue oneF2 [ (i = 0) -> true ] -- test1 : PathP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true F2EqBool : Path U F2 bool = inv U bool F2 boolEqF2 @@ -179,14 +179,14 @@ testUniv1 (A : U) : Path U A A = ntestUniv1 (A:U) : Path 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) * PathP ( 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) * PathP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * PathP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> PathP ( ((x0 : A) * PathP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * PathP ( 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) * PathP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> + [ (i = 0) -> comp (<_>U) A [ (l = 0) -> Glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * PathP ( 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) * PathP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * PathP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> PathP ( ((x0 : A) * PathP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * PathP ( 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) * PathP ( 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) * PathP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * PathP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> PathP ( ((x0 : A) * PathP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * PathP ( 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 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) * PathP ( 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) * PathP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * PathP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> PathP ( ((x0 : bool) * PathP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * PathP ( 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) * PathP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : 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) * PathP ( 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) * PathP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * PathP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> PathP ( ((x0 : bool) * PathP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * PathP ( 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) * PathP ( 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) * PathP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * PathP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> PathP ( ((x0 : bool) * PathP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * PathP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] diff --git a/examples/demo.ctt b/examples/demo.ctt index a40fe3d..966da19 100644 --- a/examples/demo.ctt +++ b/examples/demo.ctt @@ -383,7 +383,7 @@ equal: (A = B) ~ (A ~ B) Glueing is a weaker form of this for producing non-trivial equalities -from equivalences. In particular glueing gives a map from Equiv(A,B) +from equivalences. In particular Glueing gives a map from Equiv(A,B) to A = B. This weak form of univalence is useful for developing a lot of examples. For examples see: diff --git a/examples/equiv.ctt b/examples/equiv.ctt index e23bce3..1e644cf 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -25,7 +25,7 @@ idIsEquiv (A : U) : isEquiv A A (idfun A) = ,\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2) equivPath (T A : U) (f : T -> A) (p : isEquiv T A f) : Path U T A = - glue A [ (i=0) -> (T,f,p), (i=1) -> (A,idfun A, idIsEquiv A)] + Glue A [ (i=0) -> (T,f,p), (i=1) -> (A,idfun A, idIsEquiv A)] -- for univalence invEq (A B:U) (w:equiv A B) (y:B) : A = (w.2 y).1.1 @@ -67,7 +67,7 @@ transEquiv (A X:U) (p:Path U A X) : equiv A X = transDelta (A:U) : equiv A A = transEquiv A A (A) transEquivToPath (A B : U) (w : equiv A B) : Path U A B = - glue B [ (i = 1) -> (B,eB) + Glue B [ (i = 1) -> (B,eB) , (i = 0) -> (A,w) ] where eB : equiv B B = transDelta B @@ -77,7 +77,7 @@ eqToEq (A B : U) (p : Path U A B) f : equiv B B = transDelta B Ai : U = p@i g : equiv Ai B = transEquiv Ai B ( p @ (i \/ k)) - in glue B + in Glue B [ (i = 0) -> (A,e) , (i = 1) -> (B,f) , (j = 1) -> (p@i,g)] @@ -157,7 +157,7 @@ gradLemma (A B : U) (f : A -> B) (g : B -> A) isoPath (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) : Path U A B = - glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) + Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) , (i = 1) -> (B,idfun B,idIsEquiv B) ] idIsEquivGrad (A : U) : isEquiv A A (idfun A) = diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 82a1b7a..7b011c9 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -84,24 +84,24 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A lem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,idEquiv B) ,\(w : (X : U) * equiv X B) - -> let glueB : U = glue B [(i=0) -> (B,idEquiv B), (i=1) -> w] - unglueElemB : glueB -> B - = \(g : glueB) - -> unglueElem g [(i=0) -> (B,idEquiv B) + -> let GlueB : U = Glue B [(i=0) -> (B,idEquiv B), (i=1) -> w] + unglueB : GlueB -> B + = \(g : GlueB) + -> unglue g [(i=0) -> (B,idEquiv B) ,(i=1) -> w] - in (glueB - ,unglueElemB + in (GlueB + ,unglueB ,\(b : B) - -> let center : fiber glueB B unglueElemB b - = (glueElem (comp ( B) b [(i=0) -> b + -> let center : fiber GlueB B unglueB b + = (glue (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 ,(i=1) -> (w.2.2 b).1.2]) - contr (v : fiber glueB B unglueElemB b) - : Path (fiber glueB B unglueElemB b) center v - = (glueElem (comp ( B) b [(i=0) -> v.2 @ (j /\ k) + contr (v : fiber GlueB B unglueB b) + : Path (fiber GlueB B unglueB b) center v + = (glue (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 ,(i=1) -> (w.2.2 b).1.2] @@ -115,7 +115,7 @@ lem1 (B:U) : isContr ((X:U) * equiv X B) = ,(j=1) -> v.2]) in (center,contr))) --- nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> PathP ( B) y (f x))) (\(x : Sigma X (\(x : X) -> PathP ( B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> PathP ( B) y (f x0))) -> PathP ( Sigma X (\(x0 : X) -> PathP ( B) y (f x0))) x y0)))) -> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ], comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> PathP ( B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a, a),\(z : Sigma B (\(x0 : B) -> PathP ( B) a x0)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> (glueElem (comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> b ], (!1 = 1) -> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ], comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> b, (!3 = 0) -> b ], (!1 = 1) -> v.2 @ (!2 /\ !3), (!2 = 0) -> b ]))))) +-- nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> PathP ( B) y (f x))) (\(x : Sigma X (\(x : X) -> PathP ( B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> PathP ( B) y (f x0))) -> PathP ( Sigma X (\(x0 : X) -> PathP ( B) y (f x0))) x y0)))) -> (Glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : Glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglue g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glue (comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ], comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> b ]),\(v : Sigma (Glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : Glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> PathP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> PathP ( B) b (unglue x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a, a),\(z : Sigma B (\(x0 : B) -> PathP ( B) a x0)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> (glue (comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> b ], (!1 = 1) -> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ], comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> b, (!3 = 0) -> b ], (!1 = 1) -> v.2 @ (!2 /\ !3), (!2 = 0) -> b ]))))) contrSingl' (A : U) (a b : A) (p : Path A a b) : Path ((x:A) * Path A x b) (b,refl A b) (a,p) = (p @ -i, p @ -i\/j) -- 2.34.1