From 5ef8e72d03ba39f11d0dbb736b35b3ad20779883 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Rafa=C3=ABl=20Bocquet?= Date: Tue, 31 May 2016 17:00:01 +0200 Subject: [PATCH] Split csystem.ctt into category.ctt and csystem.ctt --- examples/category.ctt | 333 ++++++++++++++++++++++++++ examples/csystem.ctt | 544 +++++++++++++++++++++++++++++++++--------- 2 files changed, 762 insertions(+), 115 deletions(-) create mode 100644 examples/category.ctt diff --git a/examples/category.ctt b/examples/category.ctt new file mode 100644 index 0000000..971a7cc --- /dev/null +++ b/examples/category.ctt @@ -0,0 +1,333 @@ +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 = + comp ( A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> 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 = + comp ( 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 ( IdP p x (q@i)) hole + where + hole : IdP p x (transport p x) = comp ( p @ (i /\ j)) x [(i=0) -> <_> x] +opaque substIdP + +transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = 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 ( 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 + = (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 + ( 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 + ( 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) -> + (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) + (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) + (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) -> + (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) + (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) + (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) -> + (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) + (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) + (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 + -- = ((?, ?, ?, ?) + -- ,(?, ?, ?, ?)) + -- 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 ( lemIsCategory C isC x.1 y.1 p @ i + , lemIdPProp (isFinal C x.1) + (isFinal C y.1) + (isFinalProp C x.1) + ( 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) + (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) + (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) + (cC CA c.1 B F c.2.2.1 (cc2@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 + ( 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) -> + 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) + (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) + ( cIdC CA c.1 A D E h' j h @ -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 + ,c.2.2.2@-i + ,<_>c'.2.2.1) + in (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)) + = (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 ( isContr (p@i)) (pb3 c') diff --git a/examples/csystem.ctt b/examples/csystem.ctt index f073358..7ea839e 100644 --- a/examples/csystem.ctt +++ b/examples/csystem.ctt @@ -3,6 +3,7 @@ import prelude 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 = comp ( A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> p @ k \/ j ] @@ -25,6 +26,16 @@ opaque substIdP transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = 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 ( 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) @@ -52,6 +63,37 @@ cIdR (C : precategory) (x y : cA C) (f : cH C x y) 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 + = (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 -- | | @@ -75,6 +117,32 @@ cospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) : U * (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 + ( 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 + ( 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) @@ -82,17 +150,206 @@ isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : prop (isP (\(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) -> + (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) + (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) + (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) -> + (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) + (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) + (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) -> + (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) + (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) + (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 + -- = ((?, ?, ?, ?) + -- ,(?, ?, ?, ?)) + -- in ? -nzero (n : nat) : U = (m : nat) * Id nat n (suc m) -nzeroProp (n : nat) (x y : nzero n) : Id (nzero n) x y - = (pred (compId nat (suc x.1) n (suc y.1) (x.2@-i) y.2 @ i), - lemIdPProp (Id nat n (suc x.1)) - (Id nat n (suc y.1)) - (natSet n (suc x.1)) - (Id nat n (suc (pred (compId nat (suc x.1) n (suc y.1) (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 ( lemIsCategory C isC x.1 y.1 p @ i + , lemIdPProp (isFinal C x.1) + (isFinal C y.1) + (isFinalProp C x.1) + ( 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) + (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) + (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) + (cC CA c.1 B F c.2.2.1 (cc2@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 + ( 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) -> + 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) + (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) + ( cIdC CA c.1 A D E h' j h @ -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 + ,c.2.2.2@-i + ,<_>c'.2.2.1) + in (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)) + = (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 ( 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) @@ -136,7 +393,7 @@ C0System : U = (ob : nat -> U) * (hom : Sigma nat ob -> Sigma nat ob -> U) * (is 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 @@ -168,34 +425,58 @@ c0Square (C : C0System) (T : c0CanSq C) (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 ( 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 (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)) +-- (c0Star C (n,p0@i,Y, +-- comp ( 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 (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 (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 ( 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) @@ -513,17 +794,6 @@ isCSystem2Prop (C : C0System) : prop (isCSystem2 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) @@ -579,12 +849,13 @@ ucToC0 (C : uc) : C0System = hole 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 @@ -601,7 +872,50 @@ ucToC0 (C : uc) : C0System = hole (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, ((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 + ( 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, ((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 + (((pb n X).2 pp).1.2.1@-i) + (pb n X).1.2.2.2 + hole1 + (pb n X).2 + (transport + ( 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)) + (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, + ((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) @@ -728,74 +1042,74 @@ ucToC0 (C : uc) : C0System = hole (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) - ( 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) - (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) - (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) + -- ( 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) + -- (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) + -- (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 - ( 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 + -- ( 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 -- 2.34.1