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 = <i> 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)
* ( (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 (<i> 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 (<i>p@-i)) h)
+ (<i> (h.1, (h.2.1, hole @ i))) x (<i>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 (<i> 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 (<i> 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'))
+ ) (<i>(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
-- 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 (<i>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 (<i>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 (<i>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 (<i>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 (<i> 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 (<i> 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 (<i> 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 (<i> 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 (<i> 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 (<i> 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) (<i> fDom @ -i)))
+ (cC C q (p X)
+ (compId (cA C) (cCodom C q) X (cDom C (p X)) qCodom (<i> 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 (<i>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 (<i>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 (<i>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 (<i>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 (<i>p0@-i))).2.2.2.2.2.1)
+ (<i> (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
+ = <i> (p0@i,
+ (lemIdPProp (nzero (c0L C T0.1)) (nzero (c0L C T1.1)) (nzeroProp (c0L C T0.1)) (<i> 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))
+ (<i> 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)))
+ (<i> 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 (<i>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 (<i> 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)) (<i> 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) (<i> 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 (<i> 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 (<i> 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 (<i> 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)
+ (<i> 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 (<i> 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 (<i> 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) (<i>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, <i> 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)
+ (<i> 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) (<i> 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)
+ (<i> (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) (<i>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)) (<i> 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) (<i> 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) (<i>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 (<i> c0PDom C V @ -i)))
+ = transport
+ (<i>
+ 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))
+ (<i> 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)) (<i> gDom @ -i))
+ (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (<i>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 (<i> 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) (<i>gDom@-i)))
+ (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom (<i> 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 (<i> c0PDom C V @ -i)))
+ f'Eq)
+ = <i> 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)))
+ (<i> 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 (<i> 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 (<i> c0PDom C X @ -i)))
+ g
+ (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (<i>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 (<i> 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 (<i> c0PDom C X @ -i)))
+ g
+ (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (<i>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 (<i> 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 (<i> 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 (<i> c0PDom C X @ -i)))
+ g
+ (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (<i>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) (<i>gDom@-i)))
+ (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom (<i> 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 (<i> c0PDom C V @ -i)))
+ f'Eq)
+ (<i>cIdC C.1 f (c0P C X) g (compId (cA C.1) (cCodom C.1 f) X (cDom C.1 (c0P C X)) fCodom (<i> c0PDom C X @ -i))
+ (compId (cA C.1) (cCodom C.1 h) (c0Ft C X) (cDom C.1 g) (c0PCodom C X) (<i>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 (<i> 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
+ (<i> 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
+ (<i> 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) (<i>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) (<i>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 (<i>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 (<i>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 (<i>c0PDom C f_star@-i)))
+ (cId C.1 Y)
+ (<i> 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) (<j>c0PDom C (p9@-i)@-j)))
+ YcospanConeHom0.2.2.2.1
+ where
+ hole01 : IdP (<i> 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)
+ (<i> 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) (<i> 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 (<i> c0QDom C T1 @ -i))
+ r3 : Id (cA C.1) (cCodom C.1 YcospanConeHom0.1) (cDom C.1 (c0Q C T4))
+ = transport (<i> 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
+ (<i> 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)))
+ (<i>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'
+ = <i> 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)))
+ (<i>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 (<i> 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
+ (<i> 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)))
+ (<i>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 (<i>c0QDom C T2@-i))) f'
+ = transport (<i> 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)))
+ (<i>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 (<i>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 <i> ((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 (<i>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 (<i>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 (<i>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))
+ = <i> (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 (<i>T.2.2.2.2.1@-i)))
+ (c0FtH C g2 X g2Codom)
+ = h.2.2.2
+ p1' : IdP (<i> 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)
+ (<i> Id (cA C.1) (cDom C.1 (p0'@i)) W) g1Dom g2Dom
+ p2' : IdP (<i> 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))
+ (<i> 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 (<i>T.2.2.2.2.1@-i)), (g1Dom, T.2.2.2.2.2))))))
+ (cDom C.1 qg1) (<i> 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 (<i>T.2.2.2.2.1@-i)), (g1Dom, T.2.2.2.2.2))))))
+ (c0Star C T2) (cDom C.1 qg1)
+ (<i>plop@-i) (<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
projects / cubicaltt.git / commitdiff