{- Category Theory: - Cones; - Pullbacks. Copyright (c) Groupoid Infinity, 2014-2018. -} module cones where import sip import set import algebra isCospanConeHomProp (C: precategory) (D: cospan C) (E1 E2: cospanCone C D) (h: hom C E1.1 E2.1) : isProp (isCospanConeHom C D E1 E2 h) = propAnd (Path (hom C E1.1 D.2.1.1) (compose C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1) (Path (hom C E1.1 D.2.2.1) (compose C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1) (homSet C E1.1 D.2.1.1 (compose C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1) (homSet C E1.1 D.2.2.1 (compose C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1) cospanConePath (C: precategory) (D: cospan C) (E: cospanCone C D) : cospanConeHom C D E E = (path C E.1, pathL C E.1 D.2.1.1 E.2.1, pathL 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 = (compose C X.1 Y.1 Z.1 F.1 G.1, composition (hom C X.1 D.2.1.1) (compose C X.1 Z.1 D.2.1.1 (compose C X.1 Y.1 Z.1 F.1 G.1) Z.2.1) (compose C X.1 Y.1 D.2.1.1 F.1 (compose C Y.1 Z.1 D.2.1.1 G.1 Z.2.1)) X.2.1 (pathC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1) (composition (hom C X.1 D.2.1.1) (compose C X.1 Y.1 D.2.1.1 F.1 (compose C Y.1 Z.1 D.2.1.1 G.1 Z.2.1)) (compose C X.1 Y.1 D.2.1.1 F.1 Y.2.1) X.2.1 ( compose C X.1 Y.1 D.2.1.1 F.1 (G.2.1 @ i)) F.2.1), composition (hom C X.1 D.2.2.1) (compose C X.1 Z.1 D.2.2.1 (compose C X.1 Y.1 Z.1 F.1 G.1) Z.2.2.1) (compose C X.1 Y.1 D.2.2.1 F.1 (compose C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1)) X.2.2.1 (pathC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1) (composition (hom C X.1 D.2.2.1) (compose C X.1 Y.1 D.2.2.1 F.1 (compose C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1)) (compose C X.1 Y.1 D.2.2.1 F.1 Y.2.2.1) X.2.2.1 ( compose C X.1 Y.1 D.2.2.1 F.1 (G.2.2 @ i)) F.2.2)) isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : isProp (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)) cospanConeStructure (C: precategory) (D: cospan C) : structure C = (hasCospanCone C D ,\(x y: carrier C) (a: hasCospanCone C D x) (b: hasCospanCone C D y) -> isCospanConeHom C D (x, a) (y, b) ,\(x y: carrier C) (a: hasCospanCone C D x) (b: hasCospanCone C D y) -> isCospanConeHomProp C D (x, a) (y, b) ,\(x: carrier C) (a: hasCospanCone C D x) -> (cospanConePath C D (x, a)).2 ,\(x y z: carrier C) (a: hasCospanCone C D x) (b: hasCospanCone C D y) (c: hasCospanCone C D z) (f: hom C x y) (g: hom C y z) (Hf: isCospanConeHom C D (x, a) (y, b) f) (Hg: isCospanConeHom C D (y, b) (z, c) g) -> (cospanConeComp C D (x, a) (y, b) (z, c) (f, Hf) (g, Hg)).2 ) cospanConePrecategory (C: precategory) (D: cospan C) : precategory = sipPrecategory C (cospanConeStructure C D) isCategoryCospanCone (C: precategory) (D: cospan C) (isC: isCategory C) : isCategory (cospanConePrecategory C D) = sip C isC (cospanConeStructure C D) hole where hole: isStandardStructure C (cospanConeStructure C D) = \(x: carrier C) (a b: hasCospanCone C D x) (c: isCospanConeHom C D (x, a) (x, b) (path C x)) (d: isCospanConeHom C D (x, b) (x, a) (path C x)) -> (composition (hom C x D.2.1.1) a.1 (compose C x x D.2.1.1 (path C x) a.1) b.1 (pathL C x D.2.1.1 a.1 @-i) d.1 @ i ,composition (hom C x D.2.2.1) a.2.1 (compose C x x D.2.2.1 (path C x) a.2.1) b.2.1 (pathL C x D.2.2.1 a.2.1 @-i) d.2 @ i ,lemPathPProp (Path (hom C x D.1) (compose C x D.2.1.1 D.1 a.1 D.2.1.2) (compose C x D.2.2.1 D.1 a.2.1 D.2.2.2)) (Path (hom C x D.1) (compose C x D.2.1.1 D.1 b.1 D.2.1.2) (compose C x D.2.2.1 D.1 b.2.1 D.2.2.2)) (homSet C x D.1 (compose C x D.2.1.1 D.1 a.1 D.2.1.2) (compose C x D.2.2.1 D.1 a.2.1 D.2.2.2)) (Path (hom C x D.1) (compose C x D.2.1.1 D.1 (composition (hom C x D.2.1.1) a.1 (compose C x x D.2.1.1 (path C x) a.1) b.1 (pathL C x D.2.1.1 a.1 @-i) d.1 @ i) D.2.1.2) (compose C x D.2.2.1 D.1 (composition (hom C x D.2.2.1) a.2.1 (compose C x x D.2.2.1 (path C x) a.2.1) b.2.1 (pathL C x D.2.2.1 a.2.1 @-i) d.2 @ i) D.2.2.2)) a.2.2 b.2.2 @ i) hasPullbackProp (C: precategory) (isC: isCategory C) (D: cospan C) : isProp (hasPullback C D) = terminalProp (cospanConePrecategory C D) (isCategoryCospanCone C D isC) -- f g -- A ---> B ---> C -- j | k | l | -- v v v -- D ---> E ---> F -- h i pullbackPasting (X: precategory) (A B C D E F: carrier X) (f: hom X A B) (g: hom X B C) (h: hom X D E) (i: hom X E F) (j: hom X A D) (k: hom X B E) (l: hom X C F) (cc1: isComm X A B D E f h j k) (cc2: isComm X B C E F g i k l) (cc3: isComm X A C D F (compose X A B C f g) (compose X D E F h i) j l) (pb2: isPullback X (F, (E, i), (C, l)) (B, k, g, cc2)) (pb3: isPullback X (F, (D, compose X D E F h i), (C, l)) (A, j, compose X A B C f g, cc3)) : isPullback X (E, (D, h), (B, k)) (A, j, f, cc1) = undefined