From: Anders Mörtberg Date: Thu, 20 Oct 2016 21:28:52 +0000 (-0400) Subject: remove undefined and make csystem compile X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d9c863e94a1692c6d6301c9b935770ef85e7ba26;p=cubicaltt.git remove undefined and make csystem compile --- diff --git a/examples/csystem.ctt b/examples/csystem.ctt index 2158a97..6b50b12 100644 --- a/examples/csystem.ctt +++ b/examples/csystem.ctt @@ -452,74 +452,72 @@ ucToC0 (C : uc) : CSystem = hole (p0 (suc n) X) ) (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) - = undefined - -- = compPath (cH C.1 if_star2 (int n X.1)) - -- (cC DC f_star2 (suc n, X) (n,X.1) - -- (cC DC f_star2 (fstar n X Y f) (suc n, X) q2 (q_ n X Y f).1) - -- (p0 (suc n) X)) - -- (cC DC f_star2 (fstar n X Y f) (n,X.1) - -- q2 - -- (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (p0 (suc n) X))) - -- (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) - -- (cPathC DC f_star2 (fstar n X Y f) (suc n, X) (n,X.1) q2 (q_ n X Y f).1 (p0 (suc n) X)) - -- (compPath (cH C.1 if_star2 (int n X.1)) - -- (cC DC f_star2 (fstar n X Y f) (n,X.1) - -- q2 - -- (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (p0 (suc n) X))) - -- (cC DC f_star2 (fstar n X Y f) (n,X.1) - -- q2 - -- (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f)) - -- (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) - -- ( cC DC f_star2 (fstar n X Y f) (n,X.1) q2 - -- ((q_ n X Y f).2.1@-i)) - -- (compPath (cH C.1 if_star2 (int n X.1)) - -- (cC DC f_star2 (fstar n X Y f) (n,X.1) - -- q2 - -- (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f)) - -- (cC DC f_star2 Y (n,X.1) - -- (cC DC f_star2 (fstar n X Y f) Y q2 (p0 (suc Y.1) (fstar n X Y f).2)) - -- f) - -- (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) - -- (cPathC DC f_star2 (fstar n X Y f) Y (n, X.1) q2 (p0 (suc Y.1) (fstar n X Y f).2) f@-i) - -- (compPath (cH C.1 if_star2 (int n X.1)) - -- (cC DC f_star2 Y (n,X.1) - -- (cC DC f_star2 (fstar n X Y f) Y q2 (p0 (suc Y.1) (fstar n X Y f).2)) - -- f) - -- (cC DC f_star2 Y (n,X.1) - -- (cC DC f_star2 Z Y (p0 (suc Z.1) f_star2.2) g) - -- f) - -- (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) - -- (cC DC f_star2 Y (n,X.1) - -- ((q_ Y.1 (fstar n X Y f).2 Z g).2.1@-i) f) - -- (cPathC DC f_star2 Z Y (n, X.1) (p0 (suc Z.1) f_star2.2) g f)))) - -- opaque hole3 + = compPath (cH C.1 if_star2 (int n X.1)) + (cC DC f_star2 (suc n, X) (n,X.1) + (cC DC f_star2 (fstar n X Y f) (suc n, X) q2 (q_ n X Y f).1) + (p0 (suc n) X)) + (cC DC f_star2 (fstar n X Y f) (n,X.1) + q2 + (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (p0 (suc n) X))) + (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) + (cPathC DC f_star2 (fstar n X Y f) (suc n, X) (n,X.1) q2 (q_ n X Y f).1 (p0 (suc n) X)) + (compPath (cH C.1 if_star2 (int n X.1)) + (cC DC f_star2 (fstar n X Y f) (n,X.1) + q2 + (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (p0 (suc n) X))) + (cC DC f_star2 (fstar n X Y f) (n,X.1) + q2 + (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f)) + (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) + ( cC DC f_star2 (fstar n X Y f) (n,X.1) q2 + ((q_ n X Y f).2.1@-i)) + (compPath (cH C.1 if_star2 (int n X.1)) + (cC DC f_star2 (fstar n X Y f) (n,X.1) + q2 + (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f)) + (cC DC f_star2 Y (n,X.1) + (cC DC f_star2 (fstar n X Y f) Y q2 (p0 (suc Y.1) (fstar n X Y f).2)) + f) + (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) + (cPathC DC f_star2 (fstar n X Y f) Y (n, X.1) q2 (p0 (suc Y.1) (fstar n X Y f).2) f@-i) + (compPath (cH C.1 if_star2 (int n X.1)) + (cC DC f_star2 Y (n,X.1) + (cC DC f_star2 (fstar n X Y f) Y q2 (p0 (suc Y.1) (fstar n X Y f).2)) + f) + (cC DC f_star2 Y (n,X.1) + (cC DC f_star2 Z Y (p0 (suc Z.1) f_star2.2) g) + f) + (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F) + (cC DC f_star2 Y (n,X.1) + ((q_ Y.1 (fstar n X Y f).2 Z g).2.1@-i) f) + (cPathC DC f_star2 Z Y (n, X.1) (p0 (suc Z.1) f_star2.2) g f)))) + opaque hole3 hole4 : Path (cH C.1 if_star2 VT) (cC C.1 if_star2 (int (suc n) X) VT (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1) (pb n X).1.2.2.1) (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1 - = undefined - -- = compPath (cH C.1 if_star2 VT) - -- (cC C.1 if_star2 (int (suc n) X) VT - -- (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1) - -- (pb n X).1.2.2.1) - -- (cC C.1 if_star2 (intD (fstar n X Y f)) VT - -- q2 - -- (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT (q_ n X Y f).1 (pb n X).1.2.2.1)) - -- (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1 - -- (cPathC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) VT q2 (q_ n X Y f).1 (pb n X).1.2.2.1) - -- (compPath (cH C.1 if_star2 VT) - -- (cC C.1 if_star2 (intD (fstar n X Y f)) VT - -- q2 - -- (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT (q_ n X Y f).1 (pb n X).1.2.2.1)) - -- (cC C.1 if_star2 (intD (fstar n X Y f)) VT - -- q2 - -- (pb Y.1 (Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)).1.2.2.1) - -- (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1 - -- ( cC C.1 if_star2 (intD (fstar n X Y f)) VT q2 ((q_ n X Y f).2.2@i)) - -- (q_ Y.1 (fstar n X Y f).2 Z g).2.2) - -- opaque hole4 + = compPath (cH C.1 if_star2 VT) + (cC C.1 if_star2 (int (suc n) X) VT + (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1) + (pb n X).1.2.2.1) + (cC C.1 if_star2 (intD (fstar n X Y f)) VT + q2 + (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT (q_ n X Y f).1 (pb n X).1.2.2.1)) + (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1 + (cPathC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) VT q2 (q_ n X Y f).1 (pb n X).1.2.2.1) + (compPath (cH C.1 if_star2 VT) + (cC C.1 if_star2 (intD (fstar n X Y f)) VT + q2 + (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT (q_ n X Y f).1 (pb n X).1.2.2.1)) + (cC C.1 if_star2 (intD (fstar n X Y f)) VT + q2 + (pb Y.1 (Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)).1.2.2.1) + (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1 + ( cC C.1 if_star2 (intD (fstar n X Y f)) VT q2 ((q_ n X Y f).2.2.1@i)) + (q_ Y.1 (fstar n X Y f).2 Z g).2.2.1) + opaque hole4 pph : cospanConeHom C.1 (cs n X) pp (pb n X).1 = transport