--- /dev/null
+module category where
+import prelude
+import sigma
+import equiv
+import nat
+
+lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p =
+ <j i> comp (<k> A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <k> p @ k \/ j ]
+opaque lemReflComp
+
+lemReflComp' (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a b b p (<_> b)) p =
+ <j i> comp (<k> A) (p @ i) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <_> b ]
+opaque lemReflComp'
+
+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
+opaque lemIdPProp
+
+substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y
+ = transport (<i> IdP p x (q@i)) hole
+ where
+ hole : IdP p x (transport p x) = <i> comp (<j> p @ (i /\ j)) x [(i=0) -> <_> x]
+opaque substIdP
+
+transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]
+opaque transRefl
+
+isContrProp (A : U) (p : isContr A) (x y : A) : Id A x y = compId A x p.1 y (<i> p.2 x @ -i) (p.2 y)
+
+equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =
+ (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
+opaque equivProp
+
+idProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : Id U A B
+ = equivId A B (equivProp A B AProp BProp F G).1 (equivProp A B AProp BProp F G).2
+opaque idProp
+
+--
+
+categoryData : U = (A : U) * (A -> A -> U)
+
+isPrecategory (C : categoryData) : U =
+ let A : U = C.1
+ hom : A -> A -> U = C.2
+ in (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)
+ * (cIdL : (x y : A) -> (f : hom x y) -> Id (hom x y) (c x x y (id x) f) f)
+ * (cIdR : (x y : A) -> (f : hom x y) -> Id (hom x y) (c x y y f (id y)) f)
+ * ( (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)))
+
+precategory : U = (C : categoryData) * isPrecategory C
+
+cA (C : precategory) : U = C.1.1
+cH (C : precategory) (a b : cA C) : U = C.1.2 a b
+cHSet (C : precategory) (a b : cA C) : set (cH C a b) = C.2.1 a b
+cC (C : precategory) (x y z : cA C) (f : cH C x y) (g : cH C y z) : cH C x z = C.2.2.2.1 x y z f g
+cId (C : precategory) (x : cA C) : cH C x x = C.2.2.1 x
+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.1 x y f
+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.1 x y f
+cIdC (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 x y z w f g h
+
+--
+
+iso (C : precategory) (A B : cA C) : U
+ = (f : cH C A B) * (g : cH C B A)
+ * (_ : Id (cH C A A) (cC C A B A f g) (cId C A))
+ * (Id (cH C B B) (cC C B A B g f) (cId C B))
+
+isoId (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A))
+eqToIso (C : precategory) (A B : cA C) (p : Id (cA C) A B) : iso C A B
+ = J (cA C) A (\(B : cA C) -> \(p : Id (cA C) A B) -> iso C A B) (isoId C A) B p
+isCategory (C : precategory) : U = (A : cA C) -> isContr ((B : cA C) * iso C A B)
+lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B) : Id (cA C) A B
+ = <i> (isContrProp ((B : cA C) * iso C A B) (isC A) (A, isoId C A) (B, e) @ i).1
+
+-- f'
+-- W -----> Z
+-- | |
+-- g' | | g
+-- | |
+-- V V
+-- Y -----> X
+-- f
+
+homTo (C : precategory) (X : cA C) : U = (Y : cA C) * cH C Y X
+cospan (C : precategory) : U
+ = (X : cA C) * (_ : homTo C X) * homTo C X
+cospanCone (C : precategory) (D : cospan C) : U
+ = (W : cA C) * (f : cH C W D.2.1.1) * (g : cH C W D.2.2.1)
+ * Id (cH C W D.1)
+ (cC C W D.2.1.1 D.1 f D.2.1.2)
+ (cC C W D.2.2.1 D.1 g D.2.2.2)
+cospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) : U
+ = (h : cH C E1.1 E2.1)
+ * (_ : Id (cH C E1.1 D.2.1.1) (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1)
+ * (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1)
+cospanConeId (C : precategory) (D : cospan C) (E : cospanCone C D) : cospanConeHom C D E E
+ = (cId C E.1, cIdL C E.1 D.2.1.1 E.2.1, cIdL C E.1 D.2.2.1 E.2.2.1)
+cospanConeComp (C : precategory) (D : cospan C) (X Y Z : cospanCone C D)
+ (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) : cospanConeHom C D X Z
+ = (cC C X.1 Y.1 Z.1 F.1 G.1
+ ,compId (cH C X.1 D.2.1.1)
+ (cC C X.1 Z.1 D.2.1.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.1)
+ (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
+ X.2.1
+ (cIdC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1)
+ (compId (cH C X.1 D.2.1.1)
+ (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
+ (cC C X.1 Y.1 D.2.1.1 F.1 Y.2.1)
+ X.2.1
+ (<i> cC C X.1 Y.1 D.2.1.1 F.1 (G.2.1 @ i))
+ F.2.1)
+ ,compId (cH C X.1 D.2.2.1)
+ (cC C X.1 Z.1 D.2.2.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.2.1)
+ (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
+ X.2.2.1
+ (cIdC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1)
+ (compId (cH C X.1 D.2.2.1)
+ (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
+ (cC C X.1 Y.1 D.2.2.1 F.1 Y.2.2.1)
+ X.2.2.1
+ (<i> cC C X.1 Y.1 D.2.2.1 F.1 (G.2.2 @ i))
+ F.2.2))
+
+isPullback (C : precategory) (D : cospan C) (E : cospanCone C D) : U
+ = (h : cospanCone C D) -> isContr (cospanConeHom C D h E)
+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
+
+cospanConePrecategory (C : precategory) (D : cospan C) : precategory
+ = ((cospanCone C D, cospanConeHom C D)
+ ,(\(X Y : cospanCone C D) -> setSig (cH C X.1 Y.1)
+ (\(h : cH C X.1 Y.1) ->
+ (_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
+ * (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1))
+ (cHSet C X.1 Y.1)
+ (\(h : cH C X.1 Y.1) -> setSig (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
+ (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) ->
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1))
+ (propSet (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1))
+ (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) ->
+ (propSet (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)))))
+ ,cospanConeId C D
+ ,cospanConeComp C D
+ ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) ->
+ <i> (cIdL C X.1 Y.1 F.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1)
+ (cospanConeComp C D X X Y (cospanConeId C D X) F).2.1
+ F.2.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1)
+ (cospanConeComp C D X X Y (cospanConeId C D X) F).2.2
+ F.2.2 @ i)
+ ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) ->
+ <i> (cIdR C X.1 Y.1 F.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1)
+ (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.1
+ F.2.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1)
+ (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.2
+ F.2.2 @ i)
+ ,\(X Y Z W : cospanCone C D) (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) (H : cospanConeHom C D Z W) ->
+ <i> (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1)
+ (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1)
+ (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.1) X.2.1)
+ (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.1
+ (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1)
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1)
+ (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.2.1) X.2.2.1)
+ (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.2
+ (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.2 @ i))
+
+isCategoryCospanCone (C : precategory) (isC : isCategory C) (D : cospan C)
+ : isCategory (cospanConePrecategory C D)
+ = undefined
+ -- = \(A : cospanCone C D) ->
+ -- let p (X : (B : cospanCone C D) * iso (cospanConePrecategory C D) A B)
+ -- : Id ((B : cospanCone C D) * iso (cospanConePrecategory C D) A B) (A, isoId (cospanConePrecategory C D) A) X
+ -- = <i> ((?, ?, ?, ?)
+ -- ,(?, ?, ?, ?))
+ -- in ?
+
+isFinal (C : precategory) (A : cA C) : U = (B : cA C) -> isContr (cH C B A)
+isFinalProp (C : precategory) (A : cA C) : prop (isFinal C A)
+ = propPi (cA C) (\(B : cA C) -> isContr (cH C B A))
+ (\(B : cA C) -> propIsContr (cH C B A))
+
+hasFinal (C : precategory) : U = (A : cA C) * isFinal C A
+
+hasFinalProp (C : precategory) (isC : isCategory C) : prop (hasFinal C)
+ = \(x y : hasFinal C) ->
+ let p : iso C x.1 y.1
+ = ((y.2 x.1).1, (x.2 y.1).1
+ , isContrProp (cH C x.1 x.1) (x.2 x.1) (cC C x.1 y.1 x.1 (y.2 x.1).1 (x.2 y.1).1) (cId C x.1)
+ , isContrProp (cH C y.1 y.1) (y.2 y.1) (cC C y.1 x.1 y.1 (x.2 y.1).1 (y.2 x.1).1) (cId C y.1))
+ in <i> ( lemIsCategory C isC x.1 y.1 p @ i
+ , lemIdPProp (isFinal C x.1)
+ (isFinal C y.1)
+ (isFinalProp C x.1)
+ (<i> isFinal C (lemIsCategory C isC x.1 y.1 p @ i))
+ x.2 y.2 @ i)
+
+hasPullbackProp (C : precategory) (isC : isCategory C) (D : cospan C) : prop (hasPullback C D)
+ = hasFinalProp (cospanConePrecategory C D) (isCategoryCospanCone C isC D)
+
+isCommutative (CA : precategory)
+ (A B C D : cA CA)
+ (f : cH CA A B) (g : cH CA C D)
+ (h : cH CA A C) (i : cH CA B D)
+ : U = Id (cH CA A D) (cC CA A C D h g) (cC CA A B D f i)
+
+pullbackPasting
+ (CA : precategory)
+ (A B C D E F : cA CA)
+ (f : cH CA A B) (g : cH CA B C)
+ (h : cH CA D E) (i : cH CA E F)
+ (j : cH CA A D) (k : cH CA B E) (l : cH CA C F)
+ (cc1 : isCommutative CA A B D E f h j k)
+ (cc2 : isCommutative CA B C E F g i k l)
+ (cc3 : isCommutative CA A C D F (cC CA A B C f g) (cC CA D E F h i) j l)
+ (pb2 : isPullback CA (F, (E, i), (C, l)) (B, k, g, cc2))
+ (pb3 : isPullback CA (F, (D, cC CA D E F h i), (C, l)) (A, j, cC CA A B C f g, cc3))
+ : isPullback CA (E, (D, h), (B, k)) (A, j, f, cc1)
+ = \(c : cospanCone CA (E, (D, h), (B, k))) ->
+ let hole : Id (cH CA c.1 F)
+ (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ = compId (cH CA c.1 F)
+ (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (<n>cIdC CA c.1 D E F c.2.1 h i@-n)
+ (compId (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (<n>cC CA c.1 E F (c.2.2.2@n) i)
+ (compId (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
+ (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (cIdC CA c.1 B E F c.2.2.1 k i)
+ (compId (cH CA c.1 F)
+ (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
+ (cC CA c.1 B F c.2.2.1 (cC CA B C F g l))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (<n>cC CA c.1 B F c.2.2.1 (cc2@n))
+ (<n>cIdC CA c.1 B C F c.2.2.1 g l@-n))))
+ c' : cospanCone CA (F, (D, cC CA D E F h i), (C, l))
+ = (c.1
+ ,c.2.1
+ ,cC CA c.1 B C c.2.2.1 g
+ ,hole)
+
+ hole2 : Id (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ = compId (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (cIdC CA c.1 D E F c.2.1 h i)
+ hole
+ cc : cospanCone CA (F, (E, i), (C, l))
+ = (c.1, cC CA c.1 D E c.2.1 h, c'.2.2.1, hole2)
+
+ p0 (h' : cH CA c.1 A) (p : Id (cH CA c.1 D) (cC CA c.1 A D h' j) c.2.1)
+ : Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+ (Id (cH CA c.1 C) (cC CA c.1 A C h' (cC CA A B C f g)) c'.2.2.1)
+ = transport
+ (<i> Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+ (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ i) c'.2.2.1))
+ (idProp (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+ (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
+ (cHSet CA c.1 B (cC CA c.1 A B h' f) c.2.2.1)
+ (cHSet CA c.1 C (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
+ (\(p:Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) ->
+ <i> cC CA c.1 B C (p@i) g)
+ (\(p1:Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) ->
+ let h1 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
+ = (cC CA c.1 A B h' f
+ ,compId (cH CA c.1 E)
+ (cC CA c.1 B E (cC CA c.1 A B h' f) k)
+ (cC CA c.1 A E h' (cC CA A B E f k))
+ (cC CA c.1 D E c.2.1 h)
+ (cIdC CA c.1 A B E h' f k)
+ (compId (cH CA c.1 E)
+ (cC CA c.1 A E h' (cC CA A B E f k))
+ (cC CA c.1 A E h' (cC CA A D E j h))
+ (cC CA c.1 D E c.2.1 h)
+ (<i>cC CA c.1 A E h' (cc1@-i))
+ (compId (cH CA c.1 E)
+ (cC CA c.1 A E h' (cC CA A D E j h))
+ (cC CA c.1 D E (cC CA c.1 A D h' j) h)
+ (cC CA c.1 D E c.2.1 h)
+ (<i> cIdC CA c.1 A D E h' j h @ -i)
+ (<i> cC CA c.1 D E (p@i) h)))
+ ,p1)
+ h2 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
+ = (c.2.2.1
+ ,<i>c.2.2.2@-i
+ ,<_>c'.2.2.1)
+ in <n> (isContrProp (cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)) (pb2 cc) h1 h2 @ n).1
+ ))
+
+ p : Id U (cospanConeHom CA (F, (D, cC CA D E F h i), (C, l)) c' (A, j, cC CA A B C f g, cc3))
+ (cospanConeHom CA (E, (D, h), (B, k)) c (A, j, f, cc1))
+ = <i> (h : cH CA c.1 A)
+ * (p : Id (cH CA c.1 D) (cC CA c.1 A D h j) c.2.1)
+ * (p0 h p @ -i)
+ in transport (<i> isContr (p@i)) (pb3 c')
import sigma
import equiv
import nat
+import category
lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p =
<j i> comp (<k> A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <k> p @ k \/ j ]
transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]
opaque transRefl
+isContrProp (A : U) (p : isContr A) (x y : A) : Id A x y = compId A x p.1 y (<i> p.2 x @ -i) (p.2 y)
+
+equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =
+ (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
+opaque equivProp
+
+idProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : Id U A B
+ = equivId A B (equivProp A B AProp BProp F G).1 (equivProp A B AProp BProp F G).2
+opaque idProp
+
--
categoryData : U = (A : U) * (A -> A -> U)
cIdC (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 x y z w f g h
+--
+
+iso (C : precategory) (A B : cA C) : U
+ = (f : cH C A B) * (g : cH C B A)
+ * (_ : Id (cH C A A) (cC C A B A f g) (cId C A))
+ * (Id (cH C B B) (cC C B A B g f) (cId C B))
+
+isoId (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A))
+eqToIso (C : precategory) (A B : cA C) (p : Id (cA C) A B) : iso C A B
+ = J (cA C) A (\(B : cA C) -> \(p : Id (cA C) A B) -> iso C A B) (isoId C A) B p
+isCategory (C : precategory) : U = (A : cA C) -> isContr ((B : cA C) * iso C A B)
+lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B) : Id (cA C) A B
+ = <i> (isContrProp ((B : cA C) * iso C A B) (isC A) (A, isoId C A) (B, e) @ i).1
+
+structure (X : precategory) : U
+ = (P : cA X -> U)
+ * (H : (x y : cA X) -> (a : P x) -> (b : P y) -> (f : cH X x y) -> U)
+ * (propH : (x y : cA X) -> (a : P x) -> (b : P y) -> (f : cH X x y) -> prop (H x y a b f))
+ * (Hid : (x : cA X) -> (a : P x) -> H x x a a (cId X x))
+ * ((x y z : cA X) -> (a : P x) -> (b : P y) -> (c : P z) ->
+ (f : cH X x y) -> (g : cH X y z) ->
+ H x y a b f -> H y z b c g -> H x z a c (cC X x y z f g))
+
+sP (X : precategory) (S : structure X) : cA X -> U = S.1
+sH (X : precategory) (S : structure X) : (x y : cA X) -> (a : sP X S x) -> (b : sP X S y) -> (f : cH X x y) -> U = S.2.1
+
+isStandardStructure (X : precategory) (S : structure X) : U
+ = (x : cA X) -> (a b : sP X S x) ->
+ sH X S x x a b (cId X x) -> sH X S x x b a (cId X x) ->
+ Id (sP X S x) a b
+
-- f'
-- W -----> Z
-- | |
* (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1)
cospanConeId (C : precategory) (D : cospan C) (E : cospanCone C D) : cospanConeHom C D E E
= (cId C E.1, cIdL C E.1 D.2.1.1 E.2.1, cIdL C E.1 D.2.2.1 E.2.2.1)
+cospanConeComp (C : precategory) (D : cospan C) (X Y Z : cospanCone C D)
+ (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) : cospanConeHom C D X Z
+ = (cC C X.1 Y.1 Z.1 F.1 G.1
+ ,compId (cH C X.1 D.2.1.1)
+ (cC C X.1 Z.1 D.2.1.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.1)
+ (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
+ X.2.1
+ (cIdC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1)
+ (compId (cH C X.1 D.2.1.1)
+ (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
+ (cC C X.1 Y.1 D.2.1.1 F.1 Y.2.1)
+ X.2.1
+ (<i> cC C X.1 Y.1 D.2.1.1 F.1 (G.2.1 @ i))
+ F.2.1)
+ ,compId (cH C X.1 D.2.2.1)
+ (cC C X.1 Z.1 D.2.2.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.2.1)
+ (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
+ X.2.2.1
+ (cIdC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1)
+ (compId (cH C X.1 D.2.2.1)
+ (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
+ (cC C X.1 Y.1 D.2.2.1 F.1 Y.2.2.1)
+ X.2.2.1
+ (<i> cC C X.1 Y.1 D.2.2.1 F.1 (G.2.2 @ i))
+ F.2.2))
+
isPullback (C : precategory) (D : cospan C) (E : cospanCone C D) : U
= (h : cospanCone C D) -> isContr (cospanConeHom C D h E)
isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : prop (isPullback C D 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
+cospanConePrecategory (C : precategory) (D : cospan C) : precategory
+ = ((cospanCone C D, cospanConeHom C D)
+ ,(\(X Y : cospanCone C D) -> setSig (cH C X.1 Y.1)
+ (\(h : cH C X.1 Y.1) ->
+ (_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
+ * (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1))
+ (cHSet C X.1 Y.1)
+ (\(h : cH C X.1 Y.1) -> setSig (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
+ (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) ->
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1))
+ (propSet (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1))
+ (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) ->
+ (propSet (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)))))
+ ,cospanConeId C D
+ ,cospanConeComp C D
+ ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) ->
+ <i> (cIdL C X.1 Y.1 F.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1)
+ (cospanConeComp C D X X Y (cospanConeId C D X) F).2.1
+ F.2.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1)
+ (cospanConeComp C D X X Y (cospanConeId C D X) F).2.2
+ F.2.2 @ i)
+ ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) ->
+ <i> (cIdR C X.1 Y.1 F.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
+ (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1)
+ (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.1
+ F.2.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
+ (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1)
+ (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.2
+ F.2.2 @ i)
+ ,\(X Y Z W : cospanCone C D) (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) (H : cospanConeHom C D Z W) ->
+ <i> (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1)
+ (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.1) X.2.1)
+ (cHSet C X.1 D.2.1.1 (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1)
+ (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.1) X.2.1)
+ (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.1
+ (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.1 @ i
+ ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1)
+ (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.2.1) X.2.2.1)
+ (cHSet C X.1 D.2.2.1 (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1)
+ (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.2.1) X.2.2.1)
+ (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.2
+ (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.2 @ i))
---
+isCategoryCospanCone (C : precategory) (isC : isCategory C) (D : cospan C)
+ : isCategory (cospanConePrecategory C D)
+ = undefined
+ -- = \(A : cospanCone C D) ->
+ -- let p (X : (B : cospanCone C D) * iso (cospanConePrecategory C D) A B)
+ -- : Id ((B : cospanCone C D) * iso (cospanConePrecategory C D) A B) (A, isoId (cospanConePrecategory C D) A) X
+ -- = <i> ((?, ?, ?, ?)
+ -- ,(?, ?, ?, ?))
+ -- in ?
-nzero (n : nat) : U = (m : nat) * Id nat n (suc m)
-nzeroProp (n : nat) (x y : nzero n) : Id (nzero n) x y
- = <i> (pred (compId nat (suc x.1) n (suc y.1) (<i>x.2@-i) y.2 @ i),
- lemIdPProp (Id nat n (suc x.1))
- (Id nat n (suc y.1))
- (natSet n (suc x.1))
- (<i>Id nat n (suc (pred (compId nat (suc x.1) n (suc y.1) (<i>x.2@-i) y.2 @ i))))
- x.2 y.2 @ i)
+isFinal (C : precategory) (A : cA C) : U = (B : cA C) -> isContr (cH C B A)
+isFinalProp (C : precategory) (A : cA C) : prop (isFinal C A)
+ = propPi (cA C) (\(B : cA C) -> isContr (cH C B A))
+ (\(B : cA C) -> propIsContr (cH C B A))
+
+hasFinal (C : precategory) : U = (A : cA C) * isFinal C A
+
+hasFinalProp (C : precategory) (isC : isCategory C) : prop (hasFinal C)
+ = \(x y : hasFinal C) ->
+ let p : iso C x.1 y.1
+ = ((y.2 x.1).1, (x.2 y.1).1
+ , isContrProp (cH C x.1 x.1) (x.2 x.1) (cC C x.1 y.1 x.1 (y.2 x.1).1 (x.2 y.1).1) (cId C x.1)
+ , isContrProp (cH C y.1 y.1) (y.2 y.1) (cC C y.1 x.1 y.1 (x.2 y.1).1 (y.2 x.1).1) (cId C y.1))
+ in <i> ( lemIsCategory C isC x.1 y.1 p @ i
+ , lemIdPProp (isFinal C x.1)
+ (isFinal C y.1)
+ (isFinalProp C x.1)
+ (<i> isFinal C (lemIsCategory C isC x.1 y.1 p @ i))
+ x.2 y.2 @ i)
+
+hasPullbackProp (C : precategory) (isC : isCategory C) (D : cospan C) : prop (hasPullback C D)
+ = hasFinalProp (cospanConePrecategory C D) (isCategoryCospanCone C isC D)
+
+isCommutative (CA : precategory)
+ (A B C D : cA CA)
+ (f : cH CA A B) (g : cH CA C D)
+ (h : cH CA A C) (i : cH CA B D)
+ : U = Id (cH CA A D) (cC CA A C D h g) (cC CA A B D f i)
+
+pullback2 (CA : precategory)
+ (A B C D E F : cA CA)
+ (f : cH CA A B) (g : cH CA B C)
+ (h : cH CA D E) (i : cH CA E F)
+ (j : cH CA A D) (k : cH CA B E) (l : cH CA C F)
+ (cc1 : isCommutative CA A B D E f h j k)
+ (cc2 : isCommutative CA B C E F g i k l)
+ (cc3 : isCommutative CA A C D F (cC CA A B C f g) (cC CA D E F h i) j l)
+ (pb2 : isPullback CA (F, (E, i), (C, l)) (B, k, g, cc2))
+ (pb3 : isPullback CA (F, (D, cC CA D E F h i), (C, l)) (A, j, cC CA A B C f g, cc3))
+ : isPullback CA (E, (D, h), (B, k)) (A, j, f, cc1)
+ = \(c : cospanCone CA (E, (D, h), (B, k))) ->
+ let hole : Id (cH CA c.1 F)
+ (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ = compId (cH CA c.1 F)
+ (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (<n>cIdC CA c.1 D E F c.2.1 h i@-n)
+ (compId (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (<n>cC CA c.1 E F (c.2.2.2@n) i)
+ (compId (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
+ (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (cIdC CA c.1 B E F c.2.2.1 k i)
+ (compId (cH CA c.1 F)
+ (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
+ (cC CA c.1 B F c.2.2.1 (cC CA B C F g l))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (<n>cC CA c.1 B F c.2.2.1 (cc2@n))
+ (<n>cIdC CA c.1 B C F c.2.2.1 g l@-n))))
+ c' : cospanCone CA (F, (D, cC CA D E F h i), (C, l))
+ = (c.1
+ ,c.2.1
+ ,cC CA c.1 B C c.2.2.1 g
+ ,hole)
+
+ hole2 : Id (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ = compId (cH CA c.1 F)
+ (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+ (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+ (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+ (cIdC CA c.1 D E F c.2.1 h i)
+ hole
+ cc : cospanCone CA (F, (E, i), (C, l))
+ = (c.1, cC CA c.1 D E c.2.1 h, c'.2.2.1, hole2)
+
+ p0 (h' : cH CA c.1 A) (p : Id (cH CA c.1 D) (cC CA c.1 A D h' j) c.2.1)
+ : Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+ (Id (cH CA c.1 C) (cC CA c.1 A C h' (cC CA A B C f g)) c'.2.2.1)
+ = transport
+ (<i> Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+ (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ i) c'.2.2.1))
+ (idProp (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+ (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
+ (cHSet CA c.1 B (cC CA c.1 A B h' f) c.2.2.1)
+ (cHSet CA c.1 C (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
+ (\(p:Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) ->
+ <i> cC CA c.1 B C (p@i) g)
+ (\(p1:Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) ->
+ let h1 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
+ = (cC CA c.1 A B h' f
+ ,compId (cH CA c.1 E)
+ (cC CA c.1 B E (cC CA c.1 A B h' f) k)
+ (cC CA c.1 A E h' (cC CA A B E f k))
+ (cC CA c.1 D E c.2.1 h)
+ (cIdC CA c.1 A B E h' f k)
+ (compId (cH CA c.1 E)
+ (cC CA c.1 A E h' (cC CA A B E f k))
+ (cC CA c.1 A E h' (cC CA A D E j h))
+ (cC CA c.1 D E c.2.1 h)
+ (<i>cC CA c.1 A E h' (cc1@-i))
+ (compId (cH CA c.1 E)
+ (cC CA c.1 A E h' (cC CA A D E j h))
+ (cC CA c.1 D E (cC CA c.1 A D h' j) h)
+ (cC CA c.1 D E c.2.1 h)
+ (<i> cIdC CA c.1 A D E h' j h @ -i)
+ (<i> cC CA c.1 D E (p@i) h)))
+ ,p1)
+ h2 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
+ = (c.2.2.1
+ ,<i>c.2.2.2@-i
+ ,<_>c'.2.2.1)
+ in <n> (isContrProp (cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)) (pb2 cc) h1 h2 @ n).1
+ ))
+
+ p : Id U (cospanConeHom CA (F, (D, cC CA D E F h i), (C, l)) c' (A, j, cC CA A B C f g, cc3))
+ (cospanConeHom CA (E, (D, h), (B, k)) c (A, j, f, cc1))
+ = <i> (h : cH CA c.1 A)
+ * (p : Id (cH CA c.1 D) (cC CA c.1 A D h j) c.2.1)
+ * (p0 h p @ -i)
+ in transport (<i> isContr (p@i)) (pb3 c')
+
+--
mkFt (ob : nat -> U) (ft0 : (n : nat) -> ob (suc n) -> ob n) : (n : nat) -> ob n -> Sigma nat ob = split
zero -> \(x : ob zero) -> (zero, x)
c0C (C : C0System) : precategory = ((Sigma nat C.1, C.2.1), C.2.2.1)
--- c0ASet (C : C0System) : set (cA C.1) = undefined
+c0ASet (C : C0System) : set (cA (c0C C)) = setSig nat C.1 natSet C.2.2.2.1
c0Ft (C : C0System) (x : cA (c0C C)) : cA (c0C C) = mkFt C.1 C.2.2.2.2.1 x.1 x.2
c0P (C : C0System) : (x y : cA (c0C C)) -> Id (cA (c0C C)) (c0Ft C x) y -> C.2.1 x y = C.2.2.2.2.2.1
(cC (c0C C) (c0Star C T) X (c0Ft C X) (c0Q C T) (c0P C X (c0Ft C X) (<_> (c0Ft C X)))))
= (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2).2.2.2
--- c0FtH (C : C0System) (Y X : cA C.1) (f : cH' C.1 Y X) : cH' C.1 Y (c0Ft C X)
--- = (cC C.1 (Y, X, f) (X, c0Ft C X, c0P C X) (<_> X)).2.2
+c0FtH (C : C0System) (Y X : cA (c0C C)) (f : cH (c0C C) Y X) : cH (c0C C) Y (c0Ft C X)
+ = cC (c0C C) Y X (c0Ft C X) f (c0P C X (c0Ft C X) (<_> c0Ft C X))
-- isCSystem (C : C0System) : U
--- = (s : (X : cA C.1) -> (nzX : nzero (c0L C X)) -> (Y : cA C.1) ->
--- (f : cH' C.1 Y X) ->
--- (let T : c0CanSq C = (X, nzX, Y, c0FtH C Y X f)
--- f_star : cA C.1 = c0Star C T
+-- = (s : (n : nat) -> (X : C.1 (suc n)) -> (Y : cA (c0C C)) ->
+-- (f : cH (c0C C) Y (suc n, X)) ->
+-- (let T : c0CanSq C = (n, X, Y, c0FtH C Y (suc n, X) f)
+-- f_star : cA (c0C C) = 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 (f_star, c0Ft C f_star, c0P C f_star) sCodom)
--- (cId C.1 Y))
--- * (Id (cH C.1)
--- (Y, X, f)
--- (cC C.1 s (f_star, X, c0Q C T) sCodom))))
--- * ((X : cA C.1) -> (nzX : nzero (c0L C X)) -> (Y : cA C.1) ->
--- (f : cH' C.1 Y X) ->
--- (V : cA C.1) -> (nzV : nzero (c0L C V)) ->
--- (g : cH' C.1 (c0Ft C X) (c0Ft C V)) ->
--- (let T0 : c0CanSq C = (V, nzV, c0Ft C X, g) in
--- (p0 : Id (cA C.1) X (c0Star C T0)) ->
--- (let T1 : c0CanSq C = (X, nzX, Y, c0FtH C Y X f)
--- f_star : cA C.1 = c0Star C T1
--- f' : cH C.1 = cC C.1 (Y, X, f) (c0Star C T0, V, c0Q C T0) p0
--- in Id (cH C.1)
--- (s X nzX Y f).1
--- (s V nzV Y f'.2.2).1
+-- (s : cH (c0C C) Y f_star)
+-- * (_ : Id (cH (c0C C) Y Y)
+-- (cC (c0C C) Y f_star Y s (c0P C f_star Y (c0FtStar C T)))
+-- (cId (c0C C) Y))
+-- * (Id (cH (c0C C) Y (suc n, X))
+-- f
+-- (cC (c0C C) Y f_star (suc n, X) s (c0Q C T)))))
+-- * ((n : nat) -> (X : C.1 (suc n)) -> (Y : cA (c0C C)) ->
+-- (f : cH (c0C C) Y (suc n, X)) ->
+-- (m : nat) -> (V : C.1 (suc m)) ->
+-- (g : cH (c0C C) (c0Ft C (suc n, X)) (c0Ft C (suc m, V))) ->
+-- (let T0 : c0CanSq C = (m, V, c0Ft C (suc n, X), g) in
+-- (p0 : Id (C.1 (suc n)) X (c0Star C T0).2) ->
+-- (let T1 : c0CanSq C = (n, X, Y, c0FtH C Y (suc n, X) f)
+-- f_star : cA (c0C C) = c0Star C T1
+-- Qg : cH (c0C C) (suc n, X) (suc m, V) = transport (<i> cH (c0C C) (suc n, p0@-i) (suc m, V)) (c0Q C T0)
+-- f' : cH (c0C C) Y (suc m, V)
+-- = cC (c0C C) Y (suc n, X) (suc m, V) f Qg
+-- T2 : c0CanSq C = (m, V, Y, c0FtH C Y (suc m, V) f')
+-- f'_star : cA (c0C C) = c0Star C T2
+-- p1 : Id (cA (c0C C)) f_star f'_star
+-- = compId (cA (c0C C))
+-- f_star
+-- (c0Star C (m, V, Y, cC (c0C C) Y (c0Ft C (suc n, X)) (c0Ft C (suc m, V)) (c0FtH C Y (suc n, X) f) g))
+-- f'_star
+-- (compId (cA (c0C C))
+-- f_star
+-- (c0Star C (n,(c0Star C T0).2,Y,transport (<i>cH (c0C C) Y (c0Ft C (suc n, p0@i))) (c0FtH C Y (suc n, X) f)))
+-- (c0Star C (m, V, Y, cC (c0C C) Y (c0Ft C (suc n, X)) (c0Ft C (suc m, V)) (c0FtH C Y (suc n, X) f) g))
+-- (<i>c0Star C (n,p0@i,Y,
+-- comp (<j> cH (c0C C) Y (c0Ft C (suc n, p0@(i/\j))))
+-- (c0FtH C Y (suc n, X) f)
+-- [(i=0)-><_>c0FtH C Y (suc n, X) f]))
+-- (compId (cA (c0C C))
+-- (c0Star C (n,(c0Star C T0).2,Y,transport (<i>cH (c0C C) Y (c0Ft C (suc n, p0@i))) (c0FtH C Y (suc n, X) f)))
+-- (c0Star C (n,(c0Star C T0).2,Y,transport (<i>cH (c0C C) Y (c0FtStar C T0@-i)) (c0FtH C Y (suc n, X) f)))
+-- (c0Star C (m, V, Y, cC (c0C C) Y (c0Ft C (suc n, X)) (c0Ft C (suc m, V)) (c0FtH C Y (suc n, X) f) g))
+-- ?
+-- (C.2.2.2.2.2.2.2.2 m V (c0Ft C (suc n, X)) g Y (c0FtH C Y (suc n, X) f)).1))
+-- ?
+-- in IdP (<i> cH (c0C C) Y (p1@i))
+-- (f_star, (s n X Y f).1)
+-- (f'_star, (s m V Y f').1)
-- )))
isCSystem2Cospan (C : C0System) (T : c0CanSq C) : cospan (c0C C)
-- hole1 : isContr (cospanConeHom C.1 (isCSystem2Cospan C T) h (isCSystem2CospanCone C T)) = undefined
--
-iso (C : precategory) (A B : cA C) : U
- = (f : cH C A B) * (g : cH C B A)
- * (_ : Id (cH C A A) (cC C A B A f g) (cId C A))
- * (Id (cH C B B) (cC C B A B g f) (cId C B))
-isoId (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A))
-eqToIso (C : precategory) (A B : cA C) (p : Id (cA C) A B) : iso C A B
- = J (cA C) A (\(B : cA C) -> \(p : Id (cA C) A B) -> iso C A B) (isoId C A) B p
-isCategory (C : precategory) : U = (A B : cA C) -> isEquiv (Id (cA C) A B) (iso C A B) (eqToIso C A B)
-
-isFinal (C : precategory) (A : cA C) : U = (B : cA C) -> isContr (cH C B A)
-hasFinal (C : precategory) : U = (A : cA C) * isFinal C A
uc : U
= (C : precategory)
q_ (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
: (q : homD (fstar n X Y f) (suc n, X))
- * (_ : Id (homD (fstar n X Y f) (n, X.1))
- (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f)
- (cC DC (fstar n X Y f) (suc n, X) (n, X.1) q (p0 (suc n) X)))
- * Id (cH C.1 (intD (fstar n X Y f)) VT)
- (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT q (pb n X).1.2.2.1)
- (pb Y.1 (Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)).1.2.2.1
+ * (qSq : Id (homD (fstar n X Y f) (n, X.1))
+ (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f)
+ (cC DC (fstar n X Y f) (suc n, X) (n, X.1) q (p0 (suc n) X)))
+ * (_ : Id (cH C.1 (intD (fstar n X Y f)) VT)
+ (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT q (pb n X).1.2.2.1)
+ (pb Y.1 (Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)).1.2.2.1)
+ * isPullback DC ((n, X.1), (Y, f), ((suc n, X), p0 (suc n) X)) (fstar n X Y f, p0 (suc Y.1) (fstar n X Y f).2, q, qSq)
= let f_star : obD = fstar n X Y f
if_star : cA C.1 = intD f_star
gF : cH C.1 (intD Y) V = cC C.1 (intD Y) (int n X.1) V f X.2
(pb Y.1 (Y.2, gF)).1.2.2.2
pp : cospanCone C.1 (cs n X)
= (if_star, pg, qq, hole0)
- in (((pb n X).2 pp).1.1, <i>((pb n X).2 pp).1.2.1@-i, ((pb n X).2 pp).1.2.2)
+ q : homD (fstar n X Y f) (suc n, X) = ((pb n X).2 pp).1.1
+ hole1 : Id (cH C.1 if_star V)
+ (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
+ (cC C.1 if_star VT V (cC C.1 if_star (int (suc n) X) VT q (pb n X).1.2.2.1) p)
+ = transport
+ (<i> Id (cH C.1 if_star V)
+ (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
+ (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2 @ -i) p))
+ (pb Y.1 (Y.2, gF)).1.2.2.2
+ pbD : isPullback C.1 (int n X.1, (intD Y, f), (int (suc n) X, p0 (suc n) X))
+ (if_star, p0 (suc Y.1) (fstar n X Y f).2, q, <i>((pb n X).2 pp).1.2.1@-i)
+ = pullback2 C.1
+ if_star (int (suc n) X) VT
+ (intD Y) (int n X.1) V
+ q (pb n X).1.2.2.1
+ f X.2
+ (p0 (suc Y.1) f_star.2) (p0 (suc n) X) p
+ (<i>((pb n X).2 pp).1.2.1@-i)
+ (pb n X).1.2.2.2
+ hole1
+ (pb n X).2
+ (transport
+ (<i> isPullback C.1 (cs Y.1 f_star.2)
+ ((pb Y.1 f_star.2).1.1
+ ,(pb Y.1 f_star.2).1.2.1
+ ,((pb n X).2 pp).1.2.2@-i
+ ,lemIdPProp
+ (Id (cH C.1 if_star V) (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
+ (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@1) p))
+ (Id (cH C.1 if_star V) (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
+ (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@0) p))
+ (cHSet C.1 if_star V (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
+ (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@1) p))
+ (<i>Id (cH C.1 if_star V) (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
+ (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@-i) p))
+ (pb Y.1 f_star.2).1.2.2.2 hole1 @ i
+ ))
+ (pb Y.1 f_star.2).2)
+ in (q,
+ <i>((pb n X).2 pp).1.2.1@-i,
+ ((pb n X).2 pp).1.2.2,
+ \(A : cospanCone DC ((n, X.1), (Y, f), ((suc n, X), p0 (suc n) X))) ->
+ pbD (intD A.1, A.2.1, A.2.2.1, A.2.2.2)
+ )
sqD (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
: (f_star : ob (suc Y.1)) * (ftf : Id obD (Y.1, ft0 Y.1 f_star) Y)
(p0 (suc n) X)
)
(cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F)
- -- = undefined
- = compId (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)
- (cIdC 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))
- (compId (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)
- (<i> cC DC f_star2 (fstar n X Y f) (n,X.1) q2
- ((q_ n X Y f).2.1@-i))
- (compId (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)
- (<i>cIdC 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)
- (compId (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)
- (<i>cC DC f_star2 Y (n,X.1)
- ((q_ Y.1 (fstar n X Y f).2 Z g).2.1@-i) f)
- (cIdC DC f_star2 Z Y (n, X.1) (p0 (suc Z.1) f_star2.2) g f))))
- opaque hole3
+ = undefined
+ -- = compId (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)
+ -- (cIdC 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))
+ -- (compId (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)
+ -- (<i> cC DC f_star2 (fstar n X Y f) (n,X.1) q2
+ -- ((q_ n X Y f).2.1@-i))
+ -- (compId (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)
+ -- (<i>cIdC 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)
+ -- (compId (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)
+ -- (<i>cC DC f_star2 Y (n,X.1)
+ -- ((q_ Y.1 (fstar n X Y f).2 Z g).2.1@-i) f)
+ -- (cIdC DC f_star2 Z Y (n, X.1) (p0 (suc Z.1) f_star2.2) g f))))
+ -- opaque hole3
hole4 : Id (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
- = compId (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
- (cIdC 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)
- (compId (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
- (<i> 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
+ = undefined
+ -- = compId (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
+ -- (cIdC 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)
+ -- (compId (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
+ -- (<i> 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
pph : cospanConeHom C.1 (cs n X) pp (pb n X).1
= transport
projects / cubicaltt.git / commitdiff