From: Rafaël Bocquet Date: Tue, 10 May 2016 10:06:41 +0000 (+0200) Subject: Both definitions of C systems; the second one implies the first one X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f4fbd687fe7d43f19b28f1709c61d03df7872373;p=cubicaltt.git Both definitions of C systems; the second one implies the first one --- diff --git a/examples/csystem.ctt b/examples/csystem.ctt old mode 100644 new mode 100755 index 4bf843a..42abc54 --- a/examples/csystem.ctt +++ b/examples/csystem.ctt @@ -3,6 +3,11 @@ import prelude import equiv import nat +lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y + = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p + +transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = comp (<_> A) a [(i=1) -> <_>a] + precategory : U = (A : U) * (ASet : set A) * (hom : A -> A -> U) * (homSet : (x y : A) -> set (hom x y)) * (id : (x : A) -> hom x x) * (c : (x y z : A) -> hom x y -> hom y z -> hom x z) @@ -11,31 +16,48 @@ precategory : U = (A : U) * (ASet : set A) * ( (x y z w : A) -> (f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Id (hom x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h))) cA (C : precategory) : U = C.1 -cH (C : precategory) : cA C -> cA C -> U = C.2.2.1 -cHS (C : precategory) : (x y : cA C) -> set (cH C x y) = C.2.2.2.1 -cId (C : precategory) : (x : cA C) -> cH C x x = C.2.2.2.2.1 -cC (C : precategory) : (x y z : cA C) -> cH C x y -> cH C y z -> cH C x z = C.2.2.2.2.2.1 -cIdL (C : precategory) : (x y : cA C) -> (f : cH C x y) -> Id (cH C x y) (cC C x x y (cId C x) f) f = C.2.2.2.2.2.2.1 -cIdR (C : precategory) : (x y : cA C) -> (f : cH C x y) -> Id (cH C x y) (cC C x y y f (cId C y)) f = C.2.2.2.2.2.2.2.1 -cAssoc (C : precategory) : (x y z w : cA C) -> (f : cH C x y) -> (g : cH C y z) -> (h : cH C z w) -> - Id (cH C x w) (cC C x z w (cC C x y z f g) h) (cC C x y w f (cC C y z w g h)) - = C.2.2.2.2.2.2.2.2 - -cIsIso (C : precategory) (x y : cA C) (f : cH C x y) : U = (g : cH C y x) * (_ : Id (cH C x x) (cC C x y x f g) (cId C x)) * (Id (cH C y y) (cC C y x y g f) (cId C y)) -cIso (C : precategory) (x y : cA C) : U = (f : cH C x y) * cIsIso C x y f - --- propCIsIso --- setCIso --- cIsoInv - -cIdToIso (C : precategory) (x y : cA C) (p : Id (cA C) x y) : cIso C x y = - J (cA C) x (\(y : cA C) -> \(p : Id (cA C) x y) -> cIso C x y) (cId C x, (cId C x, (cIdL C x x (cId C x), cIdL C x x (cId C x)))) y p - -functor (C D : precategory) : U = (F : cA C -> cA D) - * (FM : (x y : cA C) -> cH C x y -> cH D (F x) (F y)) - * (_ : (x : cA C) -> Id (cH D (F x) (F x)) (FM x x (cId C x)) (cId D (F x))) - * ( (x y z : cA C) -> (f : cH C x y) -> (g : cH C y z) -> - Id (cH D (F x) (F z)) (FM x z (cC C x y z f g)) (cC D (F x) (F y) (F z) (FM x y f) (FM y z g))) +cASet (C : precategory) : set (cA C) = C.2.1 +cH (C : precategory) : U = (x y : cA C) * (C.2.2.1 x y) +cDom (C : precategory) (x : cH C) : cA C = x.1 +cCodom (C : precategory) (x : cH C) : cA C = x.2.1 +cId (C : precategory) (x : cA C) : cH C = (x, (x, C.2.2.2.2.1 x)) +cC (C : precategory) (h1 h2 : cH C) (p : Id (cA C) (cCodom C h1) (cDom C h2)) : cH C + = (h1.1, (h2.2.1, C.2.2.2.2.2.1 h1.1 h2.1 h2.2.1 (transport ( C.2.2.1 h1.1 (p@i)) h1.2.2) h2.2.2)) +cIdL (C : precategory) (x : cA C) (h : cH C) (p : Id (cA C) x (cDom C h)) : Id (cH C) (cC C (cId C x) h p) h + = J (cA C) (cDom C h) (\(x : cA C) -> \(p : Id (cA C) (cDom C h) x) -> Id (cH C) (cC C (cId C x) h (p@-i)) h) + ( (h.1, (h.2.1, hole @ i))) x (p@-i) + where + hole : Id (C.2.2.1 h.1 h.2.1) (C.2.2.2.2.2.1 h.1 h.1 h.2.1 (transport (<_>C.2.2.1 h.1 h.1) (C.2.2.2.2.1 h.1)) h.2.2) h.2.2 + = transport ( Id (C.2.2.1 h.1 h.2.1) (C.2.2.2.2.2.1 h.1 h.1 h.2.1 (transRefl (C.2.2.1 h.1 h.1) (C.2.2.2.2.1 h.1) @ -i) h.2.2) h.2.2) (C.2.2.2.2.2.2.1 h.1 h.2.1 h.2.2) +opaque cIdL + +cIdC (C : precategory) (h1 h2 h3 : cH C) + (p : Id (cA C) (cCodom C h1) (cDom C h2)) (q : Id (cA C) (cCodom C h2) (cDom C h3)) + : Id (cH C) (cC C h1 (cC C h2 h3 q) p) (cC C (cC C h1 h2 p) h3 q) + = J (cA C) h1.2.1 + (\(A : cA C) -> \(p : Id (cA C) h1.2.1 A) -> (h2' : C.2.2.1 A h2.2.1) -> + Id (cH C) (cC C h1 (cC C (A, (h2.2.1, h2')) h3 q) p) (cC C (cC C h1 (A, (h2.2.1, h2')) p) h3 q)) + (\(h2' : C.2.2.1 h1.2.1 h2.2.1) -> + J (cA C) h2.2.1 + (\(A : cA C) -> \(q : Id (cA C) h2.2.1 A) -> (h3' : C.2.2.1 A h3.2.1) -> + Id (cH C) (cC C h1 (cC C (h1.2.1, (h2.2.1, h2')) (A, (h3.2.1, h3')) q) (<_>h1.2.1)) + (cC C (cC C h1 (h1.2.1, (h2.2.1, h2')) (<_>h1.2.1)) (A, (h3.2.1, h3')) q)) + (\(h3' : C.2.2.1 h2.2.1 h3.2.1) -> + transport ( Id (cH C) (h1.1, (h3.2.1, + C.2.2.2.2.2.1 h1.1 h1.2.1 h3.2.1 + (transRefl (C.2.2.1 h1.1 h1.2.1) h1.2.2@-i) + (C.2.2.2.2.2.1 h1.2.1 h2.2.1 h3.2.1 (transRefl (C.2.2.1 h1.2.1 h2.2.1) h2'@-i) h3'))) + (h1.1, (h3.2.1, + C.2.2.2.2.2.1 h1.1 h2.2.1 h3.2.1 + (transRefl (C.2.2.1 h1.1 h2.2.1) + (C.2.2.2.2.2.1 h1.1 h1.2.1 h2.2.1 (transRefl (C.2.2.1 h1.1 h1.2.1) h1.2.2@-i) h2')@-i) + h3')) + ) ((h1.1, (h3.2.1, C.2.2.2.2.2.2.2.2 h1.1 h1.2.1 h2.2.1 h3.2.1 h1.2.2 h2' h3'@-i))) + ) + (cDom C h3) q h3.2.2 + ) + (cDom C h2) p h2.2.2 +opaque cIdC -- f' -- W -----> Z @@ -46,73 +68,504 @@ functor (C D : precategory) : U = (F : cA C -> cA D) -- Y -----> X -- f -cospan (C : precategory) : U = (X Y Z : cA C) * (_ : cH C Y X) * cH C Z X -cospanCone (C : precategory) (S : cospan C) : U = - (W : cA C) * (f : cH C W S.2.1) * (g : cH C W S.2.2.1) * Id (cH C W S.1) (cC C W S.2.1 S.1 f S.2.2.2.1) (cC C W S.2.2.1 S.1 g S.2.2.2.2) -cospanConeHom (C : precategory) (S : cospan C) (c1 c2 : cospanCone C S) : U - = (h : cH C c1.1 c2.1) * (_ : Id (cH C c1.1 S.2.1) (cC C c1.1 c2.1 S.2.1 h c2.2.1) c1.2.1) * Id (cH C c1.1 S.2.2.1) (cC C c1.1 c2.1 S.2.2.1 h c2.2.2.1) c1.2.2.1 -isPullback (C : precategory) (S : cospan C) (c : cospanCone C S) : U - = (c2 : cospanCone C S) -> isContr (cospanConeHom C S c2 c) -hasPullback (C : precategory) (S : cospan C) : U = (c : cospanCone C S) * isPullback C S c +homTo (C : precategory) (X : cA C) : U = (Y : cA C) * (f : cH C) * (fDom : Id (cA C) (cDom C f) Y) * ( Id (cA C) (cCodom C f) X) +hom (C : precategory) (X : cA C) (Y : cA C) : U = (f : cH C) * (fDom : Id (cA C) (cDom C f) X) * ( Id (cA C) (cCodom C f) Y) -isCategory (C : precategory) : U = (x y : cA C) -> isEquiv (Id (cA C) x y) (cIso C x y) (cIdToIso C x y) -category : U = (C : precategory) * isCategory C +cospan (C : precategory) : U + = (X : cA C) * (_ : homTo C X) * homTo C X -hasFinal (C : precategory) : U = (X : cA C) - * ((Y : cA C) -> isContr (cH C Y X)) +cospanCone (C : precategory) (D : cospan C) : U + = (W : cA C) * (f : hom C W D.2.1.1) * (g : hom C W D.2.2.1) + * Id (cH C) + (cC C f.1 D.2.1.2.1 (compId (cA C) (cCodom C f.1) D.2.1.1 (cDom C D.2.1.2.1) f.2.2 (D.2.1.2.2.1@-i))) + (cC C g.1 D.2.2.2.1 (compId (cA C) (cCodom C g.1) D.2.2.1 (cDom C D.2.2.2.1) g.2.2 (D.2.2.2.2.1@-i))) --- +cospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) : U + = (h : cH C) * (hDom : Id (cA C) (cDom C h) E1.1) * (hCodom : Id (cA C) (cCodom C h) E2.1) + * (_ : Id (cH C) (cC C h E2.2.1.1 (compId (cA C) (cCodom C h) E2.1 (cDom C E2.2.1.1) hCodom (E2.2.1.2.1@-i))) E1.2.1.1) + * Id (cH C) (cC C h E2.2.2.1.1 (compId (cA C) (cCodom C h) E2.1 (cDom C E2.2.2.1.1) hCodom (E2.2.2.1.2.1@-i))) E1.2.2.1.1 + +isPullback (C : precategory) (D : cospan C) (E : cospanCone C D) : U + = (h : cospanCone C D) -> isContr (cospanConeHom C D h E) -nzero (n : nat) : U = (m : nat) * Id nat (suc m) n - -C0system : U = (C : precategory) - * (pt : hasFinal C) - * (l : cA C -> nat) - * (lPt : Id nat (l pt.1) zero) -- + l x = 0 <-> x = pt.1 - * (ft : cA C -> cA C) - * (p : (x : cA C) -> cH C x (ft x)) - * (sq : (X : cA C) -> nzero (l X) -> (Y : cA C) -> (f : cH C Y (ft X)) -> - (f' : cA C) * (_ : nzero (l f')) * (ftY : Id (cA C) (ft f') Y) - * (q : cH C f' X) - * (Id (cH C f' (ft X)) (cC C f' Y (ft X) (transport ( cH C f' (ftY @ i)) (p f')) f) (cC C f' X (ft X) q (p X))) - ) - * (_ : (X : cA C) -> (nzX : nzero (l X)) -> - (p1 : Id (cA C) (sq X nzX (ft X) (cId C (ft X))).1 X) - * (Id (cH C X X) (transport ( cH C (p1 @ i) X) (sq X nzX (ft X) (cId C (ft X))).2.2.2.1) (cId C X)) - ) - * ((X Y Z : cA C) -> (nzX : nzero (l X)) -> - (f : cH C Y (ft X)) -> (g : cH C Z Y) -> - (p1 : Id (cA C) - (sq X nzX Z (cC C Z Y (ft X) g f)).1 - (sq (sq X nzX Y f).1 (sq X nzX Y f).2.1 Z (transport ( cH C Z ((sq X nzX Y f).2.2.1 @ -i)) g)).1) - * (Id (cH C (sq X nzX Z (cC C Z Y (ft X) g f)).1 X) - (sq X nzX Z (cC C Z Y (ft X) g f)).2.2.2.1 - (cC C (sq X nzX Z (cC C Z Y (ft X) g f)).1 (sq X nzX Y f).1 X - (transport ( cH C (p1@-i) (sq X nzX Y f).1) (sq (sq X nzX Y f).1 (sq X nzX Y f).2.1 Z (transport ( cH C Z ((sq X nzX Y f).2.2.1 @ -i)) g)).2.2.2.1) - (sq X nzX Y f).2.2.2.1) - )) - -isCsystem (C : C0system) : U - = (s : (X Y : cA C.1) -> (nzX : nzero (C.2.2.1 X)) -> (f : cH C.1 Y X) -> - (let f_star_X : cA C.1 = (C.2.2.2.2.2.2.1 X nzX Y (cC C.1 Y X (C.2.2.2.2.1 X) f (C.2.2.2.2.2.1 X))).1 in - (s : cH C.1 Y f_star_X) - * (_ : Id (cH C.1 Y Y) - (cC C.1 Y f_star_X Y - s (transport ( cH C.1 f_star_X ((C.2.2.2.2.2.2.1 X nzX Y (cC C.1 Y X (C.2.2.2.2.1 X) f (C.2.2.2.2.2.1 X))).2.2.1 @ i)) (C.2.2.2.2.2.1 f_star_X))) - (cId C.1 Y)) - * (Id (cH C.1 Y X) f - (cC C.1 Y f_star_X X s (C.2.2.2.2.2.2.1 X nzX Y (cC C.1 Y X (C.2.2.2.2.1 X) f (C.2.2.2.2.2.1 X))).2.2.2.1)))) - * ((X Y : cA C.1) -> (nzX : nzero (C.2.2.1 X)) -> (f : cH C.1 Y X) -> - (V : cA C.1) -> (nzV : nzero (C.2.2.1 V)) -> (g : cH C.1 (C.2.2.2.2.1 X) (C.2.2.2.2.1 V)) -> - (_ : Id (cA C.1) X (C.2.2.2.2.2.2.1 V nzV (C.2.2.2.2.1 X) g).1) -> - (let f_star_X : cA C.1 = (C.2.2.2.2.2.2.1 X nzX Y (cC C.1 Y X (C.2.2.2.2.1 X) f (C.2.2.2.2.2.1 X))).1 in - (Id (cH C.1 Y f_star_X) (s X Y nzX f).1 ?))) +isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : prop (isPullback C D E) + = propPi (cospanCone C D) (\(h : cospanCone C D) -> isContr (cospanConeHom C D h E)) + (\(h : cospanCone C D) -> propIsContr (cospanConeHom C D h E)) + +hasPullback (C : precategory) (D : cospan C) : U = (E : cospanCone C D) * isPullback C D E -- -UC : U = (C : category) - * (CU : cA C.1) * (CUT : cA C.1) - * (p : cH C.1 CUT CU) - * (_ : (X : cA C.1) -> (f : cH C.1 X CU) -> hasPullback C.1 (CU, (CUT, (X, (p, f))))) - * (hasFinal C.1) +nzero (n : nat) : U = (m : nat) * Id nat n (suc m) +nzeroProp : (n : nat) -> prop (nzero n) = undefined + +isC0System (C : precategory) : U + = (l : cA C -> nat) + * (ft : cA C -> cA C) + * (p : cA C -> cH C) + * (pDom : (x : cA C) -> Id (cA C) (cDom C (p x)) x) + * (pCodom : (x : cA C) -> Id (cA C) (cCodom C (p x)) (ft x)) + * (sq : (X : cA C) -> nzero (l X) -> (Y : cA C) -> + (f : cH C) -> (fDom : Id (cA C) (cDom C f) Y) -> (fCodom : Id (cA C) (cCodom C f) (ft X)) -> + (f_star : cA C) * (_ : nzero (l f_star)) * (ftY : Id (cA C) (ft f_star) Y) + * (q : cH C) * (qDom : Id (cA C) (cDom C q) f_star) * (qCodom : Id (cA C) (cCodom C q) X) + * Id (cH C) + (cC C (p f_star) f + (compId (cA C) (cCodom C (p f_star)) Y (cDom C f) (compId (cA C) (cCodom C (p f_star)) (ft f_star) Y (pCodom f_star) ftY) ( fDom @ -i))) + (cC C q (p X) + (compId (cA C) (cCodom C q) X (cDom C (p X)) qCodom ( pDom X @ -i))) + ) + * ((X : cA C) -> (nzX : nzero (l X)) -> (Y : cA C) -> + (f : cH C) -> (fDom : Id (cA C) (cDom C f) Y) -> (fCodom : Id (cA C) (cCodom C f) (ft X)) -> + (Z : cA C) -> (g : cH C) -> (gDom : Id (cA C) (cDom C g) Z) -> (gCodom : Id (cA C) (cCodom C g) Y) -> + (let f_star : cA C = (sq X nzX Y f fDom fCodom).1 + nz_f_star : nzero (l f_star) = (sq X nzX Y f fDom fCodom).2.1 + p0 : Id (cA C) (ft f_star) Y = (sq X nzX Y f fDom fCodom).2.2.1 + gf : cH C = cC C g f (compId (cA C) (cCodom C g) Y (cDom C f) gCodom (fDom@-i)) + in + (p1 : Id (cA C) + (sq f_star nz_f_star Z g gDom (compId (cA C) (cCodom C g) Y (ft f_star) gCodom (p0@-i))).1 + (sq X nzX Z gf gDom fCodom).1) + * Id (cH C) + (cC C + (sq f_star nz_f_star Z g gDom (compId (cA C) (cCodom C g) Y (ft f_star) gCodom (p0@-i))).2.2.2.1 + (sq X nzX Y f fDom fCodom).2.2.2.1 + (compId (cA C) + (cCodom C (sq f_star nz_f_star Z g gDom (compId (cA C) (cCodom C g) Y (ft f_star) gCodom (p0@-i))).2.2.2.1) + f_star + (cDom C (sq X nzX Y f fDom fCodom).2.2.2.1) + ((sq f_star nz_f_star Z g gDom (compId (cA C) (cCodom C g) Y (ft f_star) gCodom (p0@-i))).2.2.2.2.2.1) + ( (sq X nzX Y f fDom fCodom).2.2.2.2.1 @ -i))) + (sq X nzX Z gf gDom fCodom).2.2.2.1 + )) + +C0System : U = (C : precategory) * isC0System C + +c0L (C : C0System) : cA C.1 -> nat = C.2.1 +c0Ft (C : C0System) : cA C.1 -> cA C.1 = C.2.2.1 + +c0P (C : C0System) : cA C.1 -> cH C.1 = C.2.2.2.1 +c0PDom (C : C0System) (X : cA C.1) : Id (cA C.1) (cDom C.1 (c0P C X)) X = C.2.2.2.2.1 X +c0PCodom (C : C0System) (X : cA C.1) : Id (cA C.1) (cCodom C.1 (c0P C X)) (c0Ft C X) = C.2.2.2.2.2.1 X + +c0CanSq (C : C0System) : U + = (X : cA C.1) * (_ : nzero (c0L C X)) * (Y : cA C.1) * (f : cH C.1) * (fDom : Id (cA C.1) (cDom C.1 f) Y) * ( Id (cA C.1) (cCodom C.1 f) (c0Ft C X)) + +c0CanSqEq (C : C0System) (T0 T1 : c0CanSq C) (p0 : Id (cA C.1) T0.1 T1.1) (p1 : Id (cH C.1) T0.2.2.2.1 T1.2.2.2.1) : Id (c0CanSq C) T0 T1 + = (p0@i, + (lemIdPProp (nzero (c0L C T0.1)) (nzero (c0L C T1.1)) (nzeroProp (c0L C T0.1)) ( nzero (c0L C (p0@i))) T0.2.1 T1.2.1 @i, + (pY@i, + (p1@i, + (lemIdPProp (Id (cA C.1) (cDom C.1 (p1@0)) (pY@0)) (Id (cA C.1) (cDom C.1 (p1@1)) (pY@1)) + (cASet C.1 (cDom C.1 (p1@0)) (pY@0)) + ( Id (cA C.1) (cDom C.1 (p1@i)) (pY@i)) T0.2.2.2.2.1 T1.2.2.2.2.1 @ i, + lemIdPProp (Id (cA C.1) (cCodom C.1 T0.2.2.2.1) (c0Ft C (p0@0))) (Id (cA C.1) (cCodom C.1 T1.2.2.2.1) (c0Ft C (p0@1))) + (cASet C.1 (cCodom C.1 T0.2.2.2.1) (c0Ft C (p0@0))) + ( Id (cA C.1) (cCodom C.1 (p1@i)) (c0Ft C (p0@i))) T0.2.2.2.2.2 T1.2.2.2.2.2 @ i + ))))) + where + pY : Id (cA C.1) T0.2.2.1 T1.2.2.1 = compId (cA C.1) T0.2.2.1 (cDom C.1 (p1@0)) T1.2.2.1 (T0.2.2.2.2.1@-i) + (compId (cA C.1) (cDom C.1 (p1@0)) (cDom C.1 (p1@1)) T1.2.2.1 ( cDom C.1 (p1@i)) T1.2.2.2.2.1) + +c0Star (C : C0System) (T : c0CanSq C) : cA C.1 + = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2).1 +c0NzStar (C : C0System) (T : c0CanSq C) : nzero (c0L C (c0Star C T)) + = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2).2.1 +c0FtStar (C : C0System) (T : c0CanSq C) + : Id (cA C.1) (c0Ft C (c0Star C T)) T.2.2.1 + = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2).2.2.1 + +c0Q (C : C0System) (T : c0CanSq C) : cH C.1 + = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2).2.2.2.1 +c0QDom (C : C0System) (T : c0CanSq C) + : Id (cA C.1) (cDom C.1 (c0Q C T)) (c0Star C T) + = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2).2.2.2.2.1 +c0QCodom (C : C0System) (T : c0CanSq C) + : Id (cA C.1) (cCodom C.1 (c0Q C T)) T.1 + = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2).2.2.2.2.2.1 + +c0Square (C : C0System) (T : c0CanSq C) + : (let f_star : cA C.1 = c0Star C T in + Id (cH C.1) + (cC C.1 (c0P C f_star) T.2.2.2.1 + (compId (cA C.1) (cCodom C.1 (c0P C f_star)) T.2.2.1 (cDom C.1 T.2.2.2.1) + (compId (cA C.1) (cCodom C.1 (c0P C f_star)) (c0Ft C f_star) T.2.2.1 (c0PCodom C f_star) (c0FtStar C T)) ( T.2.2.2.2.1 @ -i))) + (cC C.1 (c0Q C T) (c0P C T.1) + (compId (cA C.1) (cCodom C.1 (c0Q C T)) T.1 (cDom C.1 (c0P C T.1)) (c0QCodom C T) ( c0PDom C T.1 @ -i)))) + = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2).2.2.2.2.2.2 + +c0FtH (C : C0System) (f : cH C.1) (X : cA C.1) (fCodom : Id (cA C.1) (cCodom C.1 f) X) : cH C.1 + = cC C.1 f (c0P C X) (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i)) +c0FtHDom (C : C0System) (f : cH C.1) (X : cA C.1) (fCodom : Id (cA C.1) (cCodom C.1 f) X) : Id (cA C.1) (cDom C.1 (c0FtH C f X fCodom)) (cDom C.1 f) = <_> cDom C.1 f +c0FtHCodom (C : C0System) (f : cH C.1) (X : cA C.1) (fCodom : Id (cA C.1) (cCodom C.1 f) X) + : Id (cA C.1) (cCodom C.1 (c0FtH C f X fCodom)) (c0Ft C X) = undefined + +isCSystem (C : C0System) : U + = (s : (X : cA C.1) -> (nzX : nzero (c0L C X)) -> (Y : cA C.1) -> + (f : cH C.1) -> (fDom : Id (cA C.1) (cDom C.1 f) Y) -> (fCodom : Id (cA C.1) (cCodom C.1 f) X) -> + (let f_star : cA C.1 = c0Star C (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))) + in + (s : cH C.1) * (sDom : Id (cA C.1) (cDom C.1 s) Y) * (sCodom : Id (cA C.1) (cCodom C.1 s) f_star) + * (_ : Id (cH C.1) + (cC C.1 s (c0P C f_star) (compId (cA C.1) (cCodom C.1 s) f_star (cDom C.1 (c0P C f_star)) sCodom ( c0PDom C f_star @ -i))) + (cId C.1 Y)) + * (Id (cH C.1) + f + (cC C.1 s (c0Q C (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom)))))) + (compId (cA C.1) (cCodom C.1 s) f_star (cDom C.1 (c0Q C (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))))) sCodom ( c0QDom C (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))) @ -i)))))) + * ((X : cA C.1) -> (nzX : nzero (c0L C X)) -> (Y : cA C.1) -> + (f : cH C.1) -> (fDom : Id (cA C.1) (cDom C.1 f) Y) -> (fCodom : Id (cA C.1) (cCodom C.1 f) X) -> + (V : cA C.1) -> (nzV : nzero (c0L C V)) -> + (g : cH C.1) -> (gDom : Id (cA C.1) (cDom C.1 g) (c0Ft C X)) -> (gCodom : Id (cA C.1) (cCodom C.1 g) (c0Ft C V)) -> + (let T0 : c0CanSq C = (V, (nzV, (c0Ft C X, (g, (gDom, gCodom))))) in + (p0 : Id (cA C.1) X (c0Star C T0)) -> + (let T1 : c0CanSq C = (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))) + f_star : cA C.1 = c0Star C T1 + f' : cH C.1 = cC C.1 f (c0Q C T0) + (compId (cA C.1) (cCodom C.1 f) (c0Star C T0) (cDom C.1 (c0Q C T0)) + (compId (cA C.1) (cCodom C.1 f) X (c0Star C T0) fCodom p0) + ( c0QDom C T0 @ -i)) + f'Dom : Id (cA C.1) (cDom C.1 f') Y = fDom + f'Codom : Id (cA C.1) (cCodom C.1 f') V = c0QCodom C T0 + in Id (cH C.1) + (s X nzX Y f fDom fCodom).1 + (s V nzV Y f' f'Dom f'Codom).1 + ))) + +isCSystem2Cospan (C : C0System) (T : c0CanSq C) : cospan C.1 + = (c0Ft C T.1,((T.2.2.1,(T.2.2.2.1,(T.2.2.2.2.1,(T.2.2.2.2.2)))),(T.1,(c0P C T.1,(c0PDom C T.1,c0PCodom C T.1))))) + +isCSystem2CospanCone (C : C0System) (T : c0CanSq C) : cospanCone C.1 (isCSystem2Cospan C T) + = (c0Star C T,( + (c0P C (c0Star C T),(c0PDom C (c0Star C T), + (compId (cA C.1) (cCodom C.1 (c0P C (c0Star C T))) (c0Ft C (c0Star C T)) T.2.2.1 + (c0PCodom C (c0Star C T)) (c0FtStar C T)))),( + (c0Q C T,(c0QDom C T,c0QCodom C T)), + c0Square C T))) + +isCSystem2Type (C : C0System) (T : c0CanSq C) : U + = isPullback C.1 + (isCSystem2Cospan C T) + (isCSystem2CospanCone C T) +isCSystem2 (C : C0System) : U + = (T : c0CanSq C) -> isCSystem2Type C T + +isCSystem2Prop (C : C0System) : prop (isCSystem2 C) + = propPi (c0CanSq C) (\(T : c0CanSq C) -> isCSystem2Type C T) + (\(T : c0CanSq C) -> isPullbackProp C.1 (isCSystem2Cospan C T) (isCSystem2CospanCone C T)) + +isCSystem21 (C : C0System) (D : isCSystem2 C) : isCSystem C = (hole1, hole2) + where + hole1 (X : cA C.1) (nzX : nzero (c0L C X)) (Y : cA C.1) + (f : cH C.1) (fDom : Id (cA C.1) (cDom C.1 f) Y) (fCodom : Id (cA C.1) (cCodom C.1 f) X) + : (let T : c0CanSq C = (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))) + f_star : cA C.1 = c0Star C T + in + (s : cH C.1) * (sDom : Id (cA C.1) (cDom C.1 s) Y) * (sCodom : Id (cA C.1) (cCodom C.1 s) f_star) + * (_ : Id (cH C.1) + (cC C.1 s (c0P C f_star) (compId (cA C.1) (cCodom C.1 s) f_star (cDom C.1 (c0P C f_star)) sCodom ( c0PDom C f_star @ -i))) + (cId C.1 Y)) + * (Id (cH C.1) + f + (cC C.1 s (c0Q C (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom)))))) + (compId (cA C.1) (cCodom C.1 s) f_star (cDom C.1 (c0Q C T)) sCodom ( c0QDom C T @ -i))))) + = let T : c0CanSq C = (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))) + f_star : cA C.1 = c0Star C T + YcospanCone : cospanCone C.1 (isCSystem2Cospan C T) + = (Y, + ((cId C.1 Y,(<_>Y,<_>Y)), + ((f,(fDom,fCodom)), + cIdL C.1 Y (c0FtH C f X fCodom) (compId (cA C.1) Y Y (cDom C.1 f) (<_>Y) (fDom@-i))))) + YcospanConeHom : cospanConeHom C.1 (isCSystem2Cospan C T) YcospanCone (isCSystem2CospanCone C T) = (D T YcospanCone).1 + in (YcospanConeHom.1,(YcospanConeHom.2.1,(YcospanConeHom.2.2.1, (YcospanConeHom.2.2.2.1, YcospanConeHom.2.2.2.2 @ -i)))) + hole2 (X : cA C.1) (nzX : nzero (c0L C X)) (Y : cA C.1) + (f : cH C.1) (fDom : Id (cA C.1) (cDom C.1 f) Y) (fCodom : Id (cA C.1) (cCodom C.1 f) X) + (V : cA C.1) (nzV : nzero (c0L C V)) + (g : cH C.1) (gDom : Id (cA C.1) (cDom C.1 g) (c0Ft C X)) (gCodom : Id (cA C.1) (cCodom C.1 g) (c0Ft C V)) + : (let T0 : c0CanSq C = (V, (nzV, (c0Ft C X, (g, (gDom, gCodom))))) in + (p0 : Id (cA C.1) X (c0Star C T0)) -> + (let T1 : c0CanSq C = (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))) + f_star : cA C.1 = c0Star C T1 + f' : cH C.1 = cC C.1 f (c0Q C T0) + (compId (cA C.1) (cCodom C.1 f) (c0Star C T0) (cDom C.1 (c0Q C T0)) + (compId (cA C.1) (cCodom C.1 f) X (c0Star C T0) fCodom p0) + ( c0QDom C T0 @ -i)) + f'Dom : Id (cA C.1) (cDom C.1 f') Y = fDom + f'Codom : Id (cA C.1) (cCodom C.1 f') V = c0QCodom C T0 + in Id (cH C.1) + (hole1 X nzX Y f fDom fCodom).1 + (hole1 V nzV Y f' f'Dom f'Codom).1)) + = (let T0 : c0CanSq C = (V, (nzV, (c0Ft C X, (g, (gDom, gCodom))))) in + \(p0 : Id (cA C.1) X (c0Star C T0)) -> + (let T1 : c0CanSq C = (X, (nzX, (Y, (c0FtH C f X fCodom, (fDom, c0FtHCodom C f X fCodom))))) + f_star : cA C.1 = c0Star C T1 + nz_f_star : nzero (c0L C f_star) = c0NzStar C T1 + f'Eq : Id (cA C.1) (cCodom C.1 f) (cDom C.1 (c0Q C T0)) + = (compId (cA C.1) (cCodom C.1 f) (c0Star C T0) (cDom C.1 (c0Q C T0)) + (compId (cA C.1) (cCodom C.1 f) X (c0Star C T0) fCodom p0) ( c0QDom C T0 @ -i)) + f' : cH C.1 = cC C.1 f (c0Q C T0) f'Eq + f'Dom : Id (cA C.1) (cDom C.1 f') Y = fDom + f'Codom : Id (cA C.1) (cCodom C.1 f') V = c0QCodom C T0 + T2 : c0CanSq C = (V, (nzV, (Y, (c0FtH C f' V f'Codom, (f'Dom, c0FtHCodom C f' V f'Codom))))) + f'_star : cA C.1 = c0Star C T2 + + h : cH C.1 = c0FtH C f X fCodom + T4 : c0CanSq C = (c0Star C T0, (c0NzStar C T0, (Y, (h, (fDom, + (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (c0Ft C (c0Star C T0)) (c0PCodom C X) + ( (c0FtStar C T0) @ -i))))))) + T5 : c0CanSq C + = (V, (nzV, (Y, + (cC C.1 h g (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i)), (fDom, gCodom))))) + + p5 : Id (cH C.1) + (cC C.1 (c0P C (c0Star C T0)) g + (compId (cA C.1) (cCodom C.1 (c0P C (c0Star C T0))) (c0Ft C X) (cDom C.1 g) + (compId (cA C.1) (cCodom C.1 (c0P C (c0Star C T0))) (c0Ft C (c0Star C T0)) (c0Ft C X) (c0PCodom C (c0Star C T0)) (c0FtStar C T0)) ( gDom @ -i))) + (cC C.1 (c0Q C T0) (c0P C V) + (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) (c0QCodom C T0) ( c0PDom C V @ -i))) + = c0Square C T0 + + p6 : Id (cH C.1) (cC C.1 (c0P C X) g (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i))) + (cC C.1 (c0Q C T0) (c0P C V) (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + = transport + ( + Id (cH C.1) + (cC C.1 (c0P C (p0@-i)) g + (lemIdPProp (Id (cA C.1) (cCodom C.1 (c0P C (c0Star C T0))) (cDom C.1 g)) + (Id (cA C.1) (cCodom C.1 (c0P C X)) (cDom C.1 g)) + (cASet C.1 (cCodom C.1 (c0P C (c0Star C T0))) (cDom C.1 g)) + ( Id (cA C.1) (cCodom C.1 (c0P C (p0@-i))) (cDom C.1 g)) + (compId (cA C.1) (cCodom C.1 (c0P C (c0Star C T0))) (c0Ft C X) (cDom C.1 g) + (compId (cA C.1) (cCodom C.1 (c0P C (c0Star C T0))) (c0Ft C (c0Star C T0)) (c0Ft C X) (c0PCodom C (c0Star C T0)) (c0FtStar C T0)) ( gDom @ -i)) + (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i)) + @ i) + ) + (cC C.1 (c0Q C T0) (c0P C V) (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + ) p5 + + p7 : Id (cH C.1) (cC C.1 + f + (cC C.1 (c0P C X) g (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i))) + (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i))) + (cC C.1 + f + (cC C.1 (c0Q C T0) (c0P C V) (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + f'Eq) + = cC C.1 f (p6@i) + (lemIdPProp (Id (cA C.1) (cCodom C.1 f) (cDom C.1 (c0P C X))) + (Id (cA C.1) (cCodom C.1 f) (cDom C.1 (c0Q C T0))) + (cASet C.1 (cCodom C.1 f) (cDom C.1 (c0P C X))) + ( Id (cA C.1) (cCodom C.1 f) (cDom C.1 (p6@i))) + (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i)) + f'Eq @ i) + + p8 : Id (cH C.1) (cC C.1 + (cC C.1 f (c0P C X) (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i))) + g + (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i))) + (cC C.1 + (cC C.1 f (c0Q C T0) f'Eq) + (c0P C V) + (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + = compId (cH C.1) + (cC C.1 + (cC C.1 f (c0P C X) (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i))) + g + (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i))) + (cC C.1 + f + (cC C.1 (c0Q C T0) (c0P C V) (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + f'Eq) + (cC C.1 + (cC C.1 f (c0Q C T0) f'Eq) + (c0P C V) + (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + (compId (cH C.1) + (cC C.1 + (cC C.1 f (c0P C X) (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i))) + g + (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i))) + (cC C.1 f + (cC C.1 (c0P C X) g (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i))) + (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i))) + (cC C.1 + f + (cC C.1 (c0Q C T0) (c0P C V) (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + f'Eq) + (cIdC C.1 f (c0P C X) g (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom ( c0PDom C X @ -i)) + (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (gDom@-i))@-i) + p7 + ) + (cIdC C.1 f (c0Q C T0) (c0P C V) f'Eq (compId (cA C.1) (cCodom C.1 (c0Q C T0)) V (cDom C.1 (c0P C V)) f'Codom ( c0PDom C V @ -i))) + + T5eqT2 : Id (c0CanSq C) T5 T2 = c0CanSqEq C T5 T2 (<_>V) p8 + T1eqT4 : Id (c0CanSq C) T1 T4 = c0CanSqEq C T1 T4 p0 (<_>h) + + p9 : Id (cA C.1) f_star f'_star + = compId (cA C.1) f_star (c0Star C T4) f'_star + ( c0Star C (T1eqT4 @ i)) + (compId (cA C.1) (c0Star C T4) (c0Star C T5) f'_star + (C.2.2.2.2.2.2.2 V nzV (c0Ft C X) g gDom gCodom Y h fDom (c0PCodom C X)).1 + ( c0Star C (T5eqT2 @ i))) + + YcospanCone0 : cospanCone C.1 (isCSystem2Cospan C T1) + = (Y, + ((cId C.1 Y,(<_>Y,<_>Y)), + ((f,(fDom,fCodom)), + cIdL C.1 Y (c0FtH C f X fCodom) (compId (cA C.1) Y Y (cDom C.1 f) (<_>Y) (fDom@-i))))) + YcospanConeHom0 : cospanConeHom C.1 (isCSystem2Cospan C T1) YcospanCone0 (isCSystem2CospanCone C T1) = (D T1 YcospanCone0).1 + + YcospanCone1 : cospanCone C.1 (isCSystem2Cospan C T2) + = (Y, + ((cId C.1 Y,(<_>Y,<_>Y)), + ((f',(f'Dom,f'Codom)), + cIdL C.1 Y (c0FtH C f' V f'Codom) (compId (cA C.1) Y Y (cDom C.1 f') (<_>Y) (f'Dom@-i))))) + YcospanConeHom1 : cospanConeHom C.1 (isCSystem2Cospan C T2) YcospanCone1 (isCSystem2CospanCone C T2) = (D T2 YcospanCone1).1 + p1 : Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) f'_star = compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) f_star f'_star YcospanConeHom0.2.2.1 p9 + hole0 : Id (cH C.1) (cC C.1 YcospanConeHom0.1 (c0P C f'_star) + (compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) f'_star (cDom C.1 (c0P C f'_star)) p1 (c0PDom C f'_star@-i))) + (cId C.1 Y) + = compId (cH C.1) + (cC C.1 YcospanConeHom0.1 (c0P C f'_star) + (compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) f'_star (cDom C.1 (c0P C f'_star)) p1 (c0PDom C f'_star@-i))) + (cC C.1 YcospanConeHom0.1 (c0P C f_star) + (compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) f_star (cDom C.1 (c0P C f_star)) YcospanConeHom0.2.2.1 (c0PDom C f_star@-i))) + (cId C.1 Y) + ( cC C.1 YcospanConeHom0.1 (c0P C (p9@-i)) + (compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) (p9@-i) (cDom C.1 (c0P C (p9@-i))) (hole01@i) (c0PDom C (p9@-i)@-j))) + YcospanConeHom0.2.2.2.1 + where + hole01 : IdP ( Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (p9@-i)) p1 YcospanConeHom0.2.2.1 + = lemIdPProp (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) f'_star) (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) f_star) + (cASet C.1 (cCodom C.1 YcospanConeHom0.1) f'_star) + ( Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (p9@-i)) p1 YcospanConeHom0.2.2.1 + l1 : Id (cA C.1) (cCodom C.1 (c0Q C T4)) (cDom C.1 (c0Q C T0)) + = (compId (cA C.1) + (cCodom C.1 (c0Q C T4)) (c0Star C T0) (cDom C.1 (c0Q C T0)) + (c0QCodom C T4) ( c0QDom C T0 @ -i)) + l : cH C.1 = (cC C.1 (c0Q C T4) (c0Q C T0) l1) + r7 : Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T1)) + = (compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) (c0Star C T1) (cDom C.1 (c0Q C T1)) + YcospanConeHom0.2.2.1 ( c0QDom C T1 @ -i)) + r3 : Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T4)) + = transport ( Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C (T1eqT4@i)))) r7 + r6 : Id (cH C.1) (cC C.1 YcospanConeHom0.1 (c0Q C T1) r7) f + = YcospanConeHom0.2.2.2.2 + r5 : Id (cH C.1) (cC C.1 YcospanConeHom0.1 (c0Q C T4) r3) f + = transport + ( Id (cH C.1) + (cC C.1 YcospanConeHom0.1 (c0Q C (T1eqT4@i)) + (lemIdPProp (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T1))) + (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T4))) + (cASet C.1 (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T1))) + (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C (T1eqT4@i)))) + r7 r3 + @ i) + ) f) r6 + r4 : Id (cH C.1) (cC C.1 (cC C.1 YcospanConeHom0.1 (c0Q C T4) r3) (c0Q C T0) l1) f' + = cC C.1 (r5@i) (c0Q C T0) + (lemIdPProp (Id (cA C.1) (cCodom C.1 (r5@0)) (cDom C.1 (c0Q C T0))) + (Id (cA C.1) (cCodom C.1 (r5@1)) (cDom C.1 (c0Q C T0))) + (cASet C.1 (cCodom C.1 (r5@0)) (cDom C.1 (c0Q C T0))) + (Id (cA C.1) (cCodom C.1 (r5@i)) (cDom C.1 (c0Q C T0))) + l1 f'Eq@i) + r2 : Id (cH C.1) (cC C.1 YcospanConeHom0.1 l r3) f' + = compId (cH C.1) (cC C.1 YcospanConeHom0.1 l r3) (cC C.1 (cC C.1 YcospanConeHom0.1 (c0Q C T4) r3) (c0Q C T0) l1) f' + (cIdC C.1 YcospanConeHom0.1 (c0Q C T4) (c0Q C T0) r3 l1) + r4 + r1 : Id (cH C.1) l (c0Q C T5) + = (C.2.2.2.2.2.2.2 V nzV (c0Ft C X) g gDom gCodom Y h fDom (c0PCodom C X)).2 + r0 : Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T5)) + = transport ( Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (r1@i))) r3 + r9 : Id (cH C.1) (cC C.1 YcospanConeHom0.1 (c0Q C T5) r0) f' + = transport + ( Id (cH C.1) + (cC C.1 YcospanConeHom0.1 (r1@i) + (lemIdPProp (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (r1@0))) + (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (r1@1))) + (cASet C.1 (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (r1@0))) + (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (r1@i))) + r3 r0 @ i) + ) f' + ) r2 + hole1 : Id (cH C.1) (cC C.1 YcospanConeHom0.1 (c0Q C T2) + (compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) f'_star (cDom C.1 (c0Q C T2)) p1 (c0QDom C T2@-i))) f' + = transport ( Id (cH C.1) (cC C.1 YcospanConeHom0.1 (c0Q C (T5eqT2@i)) + (lemIdPProp + (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T5))) + (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T2))) + (cASet C.1 (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T5))) + (Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C (T5eqT2@i)))) + r0 (compId (cA C.1) (cCodom C.1 YcospanConeHom0.1) f'_star (cDom C.1 (c0Q C T2)) p1 (c0QDom C T2@-i)) @ i)) f') r9 + YcospanConeHom1' : cospanConeHom C.1 (isCSystem2Cospan C T2) YcospanCone1 (isCSystem2CospanCone C T2) + = (YcospanConeHom0.1, (YcospanConeHom0.2.1, (p1, + (hole0, hole1)))) + in ((D T2 YcospanCone1).2 YcospanConeHom1' @ -i).1)) + +-- stop : nat = U + +isCSystem12 (C : C0System) (D : isCSystem C) : isCSystem2 C = hole + where + hole (T : c0CanSq C) (h : cospanCone C.1 (isCSystem2Cospan C T)) + : isContr (cospanConeHom C.1 (isCSystem2Cospan C T) h (isCSystem2CospanCone C T)) = hole1 + where + X : cA C.1 = T.1 + nzX : nzero (c0L C X) = T.2.1 + Y : cA C.1 = T.2.2.1 + f_star : cA C.1 = c0Star C T + nz_f_star : nzero (c0L C f_star) = c0NzStar C T + ft_f_star : Id (cA C.1) (c0Ft C f_star) Y = c0FtStar C T + W : cA C.1 = h.1 + g1 : cH C.1 = h.2.1.1 + g1Dom : Id (cA C.1) (cDom C.1 g1) W = h.2.1.2.1 + g1Codom : Id (cA C.1) (cCodom C.1 g1) Y = h.2.1.2.2 + g2 : cH C.1 = h.2.2.1.1 + g2Dom : Id (cA C.1) (cDom C.1 g2) W = h.2.2.1.2.1 + g2Codom : Id (cA C.1) (cCodom C.1 g2) X = h.2.2.1.2.2 + + + T3 : c0CanSq C = (X, (nzX, (W, (c0FtH C g2 X g2Codom, (g2Dom, c0FtHCodom C g2 X g2Codom))))) + g2_star : cA C.1 = c0Star C T3 + + sg2 : cH C.1 = (D.1 X nzX W g2 g2Dom g2Codom).1 + sg2Codom : Id (cA C.1) (cCodom C.1 sg2) g2_star = (D.1 X nzX W g2 g2Dom g2Codom).2.2.1 + T2 : c0CanSq C = (f_star, (nz_f_star, (W, (g1, (g1Dom, compId (cA C.1) (cCodom C.1 g1) Y (c0Ft C f_star) g1Codom (ft_f_star@-i)))))) + qg1 : cH C.1 = c0Q C T2 + + plop : Id (cA C.1) + (c0Star C T2) + (c0Star C (X, (nzX, (W, (cC C.1 g1 T.2.2.2.1 (compId (cA C.1) (cCodom C.1 g1) Y (cDom C.1 T.2.2.2.1) g1Codom (T.2.2.2.2.1@-i)), (g1Dom, T.2.2.2.2.2)))))) + = (C.2.2.2.2.2.2.2 X nzX Y T.2.2.2.1 T.2.2.2.2.1 T.2.2.2.2.2 W g1 g1Dom g1Codom).1 + plop2 : Id (hom C.1 W (c0Ft C X)) + (cC C.1 g1 T.2.2.2.1 (compId (cA C.1) (cCodom C.1 g1) Y (cDom C.1 T.2.2.2.1) g1Codom (T.2.2.2.2.1@-i)), (g1Dom, T.2.2.2.2.2)) + (c0FtH C g2 X g2Codom, (g2Dom, c0FtHCodom C g2 X g2Codom)) + = (p0'@i, (p1'@i, p2'@i)) + where p0' : Id (cH C.1) + (cC C.1 g1 T.2.2.2.1 (compId (cA C.1) (cCodom C.1 g1) Y (cDom C.1 T.2.2.2.1) g1Codom (T.2.2.2.2.1@-i))) + (c0FtH C g2 X g2Codom) + = h.2.2.2 + p1' : IdP ( Id (cA C.1) (cDom C.1 (p0'@i)) W) g1Dom g2Dom + = lemIdPProp (Id (cA C.1) (cDom C.1 (p0'@0)) W) (Id (cA C.1) (cDom C.1 (p0'@1)) W) + (cASet C.1 (cDom C.1 (p0'@0)) W) + ( Id (cA C.1) (cDom C.1 (p0'@i)) W) g1Dom g2Dom + p2' : IdP ( Id (cA C.1) (cCodom C.1 (p0'@i)) (c0Ft C X)) T.2.2.2.2.2 (c0FtHCodom C g2 X g2Codom) + = lemIdPProp (Id (cA C.1) (cCodom C.1 (p0'@0)) (c0Ft C X)) (Id (cA C.1) (cCodom C.1 (p0'@1)) (c0Ft C X)) + (cASet C.1 (cCodom C.1 (p0'@0)) (c0Ft C X)) + ( Id (cA C.1) (cCodom C.1 (p0'@i)) (c0Ft C X)) T.2.2.2.2.2 (c0FtHCodom C g2 X g2Codom) + + hole21 : cH C.1 + = cC C.1 sg2 qg1 + (compId (cA C.1) + (cCodom C.1 sg2) g2_star (cDom C.1 qg1) sg2Codom + (compId (cA C.1) + g2_star + (c0Star C (X, (nzX, (W, (cC C.1 g1 T.2.2.2.1 (compId (cA C.1) (cCodom C.1 g1) Y (cDom C.1 T.2.2.2.1) g1Codom (T.2.2.2.2.1@-i)), (g1Dom, T.2.2.2.2.2)))))) + (cDom C.1 qg1) ( c0Star C (X, (nzX, (W, plop2@-i)))) + (compId (cA C.1) + (c0Star C (X, (nzX, (W, (cC C.1 g1 T.2.2.2.1 (compId (cA C.1) (cCodom C.1 g1) Y (cDom C.1 T.2.2.2.1) g1Codom (T.2.2.2.2.1@-i)), (g1Dom, T.2.2.2.2.2)))))) + (c0Star C T2) (cDom C.1 qg1) + (plop@-i) (c0QDom C T2@-i)))) + hole2 : cospanConeHom C.1 (isCSystem2Cospan C T) h (isCSystem2CospanCone C T) + = (hole21, (?, ?)) + hole1 : isContr (cospanConeHom C.1 (isCSystem2Cospan C T) h (isCSystem2CospanCone C T)) = undefined \ No newline at end of file