{- Category Theory. - Precategories. - Rezk Completion. - Initial and Terminal Objects. Copyright (c) Groupoid Infinity, 2014-2018 HoTT 9.1 Categories and precategories HoTT 9.9 The Rezk completion -} module cat where import path import proto import nat -- Category is the Algebra of Hom Functions on Ob domain cat: U = (A: U) * (A -> A -> U) -- HoTT Definition 9.1.1. Precategory Properties isPrecategory (C: cat): U = (id: (x: C.1) -> C.2 x x) * (c: (x y z:C.1) -> C.2 x y -> C.2 y z -> C.2 x z) * (homSet: (x y: C.1) -> isSet (C.2 x y)) * (left: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f) * (right: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f) * ((x y z w: C.1) -> (f: C.2 x y) -> (g: C.2 y z) -> (h: C.2 z w) -> Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h))) -- general precategory precategory: U = (C: cat) * isPrecategory C -- pointed category with zero object ptcategory: U = (C: cat) * (pre: isPrecategory C) * (z: C.1) -- zero object * ((x: C.1) -> C.2 z x -> C.2 x z) -- 0 -> A -> 0 -- Public Accessors carrier (C: precategory): U = C.1.1 hom (C: precategory) (a b: carrier C): U = C.1.2 a b homSet (C: precategory) (a b: carrier C): isSet (hom C a b) = C.2.2.2.1 a b compose (C: precategory) (x y z: carrier C) (f: hom C x y) (g: hom C y z): hom C x z = C.2.2.1 x y z f g path (C: precategory) (x: carrier C): hom C x x = C.2.1 x pathL (C: precategory) (x y: carrier C) (f: hom C x y): Path (hom C x y) (compose C x x y (path C x) f) f = C.2.2.2.2.1 x y f pathR (C: precategory) (x y: carrier C) (f: hom C x y): Path (hom C x y) (compose C x y y f (path C y)) f = C.2.2.2.2.2.1 x y f pathC (C: precategory) (x y z w: carrier C) (f: hom C x y) (g: hom C y z) (h: hom C z w): Path (hom C x w) (compose C x z w (compose C x y z f g) h) (compose C x y w f (compose C y z w g h)) = C.2.2.2.2.2.2 x y z w f g h -- iso record iso (C: precategory) (A B: carrier C): U = (f: hom C A B) * (g: hom C B A) * (_: Path (hom C A A) (compose C A B A f g) (path C A)) * ( Path (hom C B B) (compose C B A B g f) (path C B)) idIso (C: precategory) (A: carrier C): iso C A A = (path C A, path C A, pathL C A A (path C A), pathL C A A (path C A)) -- https://arxiv.org/pdf/1303.0584.pdf -- HoTT Definition 9.1.6. Category. isCategory (C: precategory): U = (A: carrier C) -> isContr ((B: carrier C) * iso C A B) category: U = (C: precategory) * isCategory C isInitial (C: precategory) (bot: carrier C): U = (x: carrier C) -> isContr (hom C bot x) isTerminal (C: precategory) (top: carrier C): U = (x: carrier C) -> isContr (hom C x top) initial (C: precategory): U = (bot: carrier C) * isInitial C bot terminal (C: precategory): U = (top: carrier C) * isTerminal C top initialProp (C: precategory) (isC: isCategory C): isProp (initial C) = undefined terminalProp (C: precategory) (isC: isCategory C): isProp (terminal C) = undefined isComm (X: precategory) (A B C D: carrier X) (f: hom X A B) (g: hom X C D) (h: hom X A C) (i: hom X B D): U = Path (hom X A D) (compose X A C D h g) (compose X A B D f i) opCat (P: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = carrier P Hom (A B: Ob): U = hom P B A id (A: Ob): Hom A A = P.2.1 A HomSet (A B: Ob): isSet (Hom A B) = homSet P B A c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = compose P C B A g f L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = pathR P B A f R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = pathL P B A f Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = pathC P D C B A h g f @ -i opPreserve (C: precategory) : Path precategory (opCat (opCat C)) C = C -- Categorical Pullback homTo (C: precategory) (X: carrier C): U = (Y: carrier C) * hom C Y X cospan (C: precategory): U = (X: carrier C) * (_: homTo C X) * homTo C X hasCospanCone (C: precategory) (D: cospan C) (W: carrier C) : U = (f: hom C W D.2.1.1) * (g: hom C W D.2.2.1) * Path (hom C W D.1) (compose C W D.2.1.1 D.1 f D.2.1.2) (compose C W D.2.2.1 D.1 g D.2.2.2) cospanCone (C: precategory) (D: cospan C): U = (W: carrier C) * hasCospanCone C D W isCospanConeHom (C: precategory) (D: cospan C) (E1 E2: cospanCone C D) (h: hom C E1.1 E2.1) : U = (_ : 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) cospanConeHom (C: precategory) (D: cospan C) (E1 E2: cospanCone C D) : U = (h: hom C E1.1 E2.1) * isCospanConeHom C D E1 E2 h isPullback (C: precategory) (D: cospan C) (E: cospanCone C D) : U = (h: cospanCone C D) -> isContr (cospanConeHom C D h E) hasPullback (C: precategory) (D: cospan C) : U = (E: cospanCone C D) * isPullback C D E isCatGroupoid (C: cat): U = (id: (x: C.1) -> C.2 x x) * (c: (x y z:C.1) -> C.2 x y -> C.2 y z -> C.2 x z) * (HomSet: (x y: C.1) -> isSet (C.2 x y)) * (inv: (x y: C.1) -> C.2 x y -> C.2 y x) * (inv_left: (x y: C.1) (p: C.2 x y) -> Path (C.2 x x) (c x y x p (inv x y p)) (id x)) * (inv_right: (x y: C.1) (p: C.2 x y) -> Path (C.2 y y) (c y x y (inv x y p) p) (id y)) * (left: (x y: C.1) (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f) * (right: (x y: C.1) (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f) * ((x y z w: C.1) (f: C.2 x y) (g: C.2 y z) (h: C.2 z w) -> Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h))) groupoid: U = (X: cat) * isCatGroupoid X PathCat (X: U): cat = (X,\(x y: X)->Path X x y) -- Sample PathGrpd (X: U) (G: isGroupoid X): groupoid = (PathCat X,id,c,G,sym X,compPathInv X,compInvPath X,L,R,Q) where Ob: U = X Hom (A B: Ob): U = Path X A B id (A: Ob): Path X A A = refl X A c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = comp ( Path X A (g@i)) f [] L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = compPathL X A B f @ -i R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = compPathR X A B f @ -i Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = compPathQ X A B C D f g h -- (n,r)-categries mutual data coinfn = coinf (x: infnat) data infnat = zero | succ (x: coinfn) inf : infnat = succ (coinf inf) infgraph : U = (vert: U) * ((x y: vert) -> infgraph) infmap (A B: infgraph): U = (tr: A.1 -> B.1) * ((x y: A.1) -> infmap (A.2 x y) (B.2 (tr x) (tr y))) data Disc (t: infgraph) = g1 | g2 (g: Disc t) (x y: (graph t g).1) graph (t: infgraph) : Disc t -> infgraph = split g1 -> t g2 g x y -> (graph t g).2 x y data Diagram (t: infgraph) (r: infnat) = d1 | d2 (p: Diagram t r) (x y: dia t r p) data Cell (t: infgraph) (r: infnat) (x: Diagram t r) = xxx dia (t: infgraph) (r: infnat) : Diagram t r -> U = split d1 -> t.1 d2 p x y -> Cell t r (d2 p x y)