{- Category Theory: http://groupoid.space/mltt/types/category/ - Examples: Set, Cat, Func, Ab. Copyright (c) Groupoid Infinity, 2014-2018. -} module category where import cat import fun import adj import set import proto import algebra import iso_sigma -- The general notion of (∞,1)-categories -- 0-cat -- 0-ob are elements, 0-hom is equivalence relation, setoid -- sets -- 1-cat -- 1-ob are sets or 0-cat, 1-hom are maps -- 2-cat-A -- 2-ob are 1-cat, 1-hom are functors/maps \ bounded -- 2-cat-B -- 2-ob are 1-cat, 2-hom are ntrans/mapsOnMaps / definition -- 3-cat-A -- 2-ob are (2-cat-A,2-cat-B), 1-hom are functors of product categories \ -- 3-cat-B -- 2-ob are (2-cat-A,2-cat-B), 2-hom are ntrans of product categories ) morphisms -- 3-cat-C -- 3-ob are (2-cat-A,2-cat-B), 3-hom are modifications / -- Enrichment -- (0-cat = Hom(A,B) = A = B) -- ↪ (1-cat = Hom(0-cat,0-cat) = set -> 0-cat) -- ↪ (2-cat = Hom(1-cat,1-cat) = (set -> 0-cat) -> 1-cat) -- ↪ (3-cat = Hom(2-cat,2-cat) = ((set -> 0-cat) -> 1-cat) -> 2-cat) -- The general notion of k-morphisms -- equiv 0-hom: U = undefined -- functor 1-hom (C D: 1-cat): U = undefined -- ntrans 2-hom (C D: 1-cat) (F G: 1-hom C D): U = undefined -- modification 3-hom (C D: 1-cat) (F G: 1-hom C D) (I J: 2-hom C D F G): U = undefined -- 1-Category of Sets Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = SET Hom (A B: Ob): U = A.1 -> B.1 id (A: Ob): Hom A A = idfun A.1 c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = o A.1 B.1 C.1 g f HomSet (A B: Ob): isSet (Hom A B) = setFun A.1 B.1 B.2 L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) 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)) = refl (Hom A D) (c A B D f (c B C D g h)) -- 2-Category with 1-hom morphisms (functors) Cat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = precategory Hom (A B: Ob): U = catfunctor A B id (A: Ob): catfunctor A A = idFunctor A c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = compFunctor A B C f g HomSet (A B: Ob): isSet (Hom A B) = undefined L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined 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)) = undefined -- AwodeyCT Definition 7.9. The functor category -- 2-Category of Functors F: X -> Y with 2-hom morphisms (natural transformations) Func (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = catfunctor X Y Hom (A B: Ob): U = ntrans X Y A B id (A: Ob): ntrans X Y A A = undefined c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = undefined HomSet (A B: Ob): isSet (Hom A B) = undefined L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined 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)) = undefined -- Lemma. Monoid Hom is Set setmonoidhom (a b: monoid) : isSet (monoidhom a b) = setSig (a.1.1 -> b.1.1) (ismonoidhom a b) setf setm where setf : isSet (a.1.1 -> b.1.1) = setPi a.1.1 (\ (_: a.1.1) -> b.1.1) (\ (_: a.1.1) -> b.1.2) setm (f: a.1.1 -> b.1.1) : isSet (ismonoidhom a b f) = propSet (ismonoidhom a b f) (propismonoidhom a b f) -- Category of Commutative Monoids CMon: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = cmonoid Hom (A B: Ob): U = cmonoidhom A B id (A: Ob): Hom A A = idmonoidhom (A.1,A.2.1) c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = monoidhomcomp (A.1, A.2.1) (B.1, B.2.1) (C.1, C.2.1) f g HomSet (A B: Ob): isSet (Hom A B) = setmonoidhom (A.1, A.2.1) (B.1, B.2.1) L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = lemma_idmonoidhom0 (A.1, A.2.1) (B.1, B.2.1) f R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = lemma_idmonoidhom1 (A.1, A.2.1) (B.1, B.2.1) 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)) = lemma_monoidcomp0 (A.1, A.2.1) (B.1, B.2.1) (C.1, C.2.1) (D.1, D.2.1) f g h -- Definition (Additive Category). abcategory: U = (X: U) -- group * (hom: X -> X -> U) -- abgroup * (id: (x: X) -> hom x x) * (c: (x y z: X) -> hom x y -> hom y z -> hom x z) * (homSet: (x y: X) -> isSet (hom x y)) * (left1: (x y: X) (f: hom x y) -> Path (hom x y) (c x x y (id x) f) f) * (right1: (x y: X) (f: hom x y) -> Path (hom x y) (c x y y f (id y)) f) * (assoc: (x y z w: X) (f: hom x y) (g: hom y z) (h: hom z w) -> Path (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))) * (z0: X) * (zer: (x: X) -> (z: X) * (l: hom z x) * (r: hom x z) * Path X z z0) * (mul: X -> X -> X) * (sum: X -> X -> X) * (pi1: (A B: X) -> hom (mul A B) A) * (pi2: (A B: X) -> hom (mul A B) B) * (inl: (A B: X) -> hom A (sum A B)) * (inr: (A B: X) -> hom B (sum A B)) -- * (precomp: (x y z w: X) (f: hom x y) (g: hom y z) (h: hom y w) -> c x y z f (sum ) -- f o (g + h) = f o g + f o h -- (f + g) o h = f o h + g o h * U --complex (a: abcategory): U -- = (objects: (n: nat) -> a.1) -- * (morphisms: (n: nat) -> a.2.1) -- * ((n: nat) -> Path a.1 (a.2.2.1 (objects n) (objects (succ n)) (objects (succ (succ n))) -- (morphisms (succ n)) (morphisms n)) (a.2.2.2.2.2.2.2.2.1)) instance: abcategory = (Ob,Hom,id,c,homSet,L,R,Q,e,zer,mul,sum,pi1,pi2,inl,inr,Ob) where Ob: U = unit Hom (x y: Ob): U = abgroup id (x: Ob): Hom x x = unitAbGroup e: Ob = tt c (x y z: Ob) (f g: abgroup): abgroup = unitAbGroup homSet (x y: Ob): isSet (abgroup) = undefined L (x y: Ob) (f: abgroup): Path (abgroup) (c x x y (id x) f) f = undefined R (x y: Ob) (f: abgroup): Path (abgroup) (c x y y f (id y)) f = undefined Q (x y z w: Ob) (f g h: abgroup): Path (abgroup) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)) = undefined zer: (x: Ob) -> (z: Ob) * (l: Hom z x) * (r: Hom x z) * Path Ob z e = undefined mul: Ob -> Ob -> Ob = \(x y: Ob) -> tt sum: Ob -> Ob -> Ob = \(x y: Ob) -> tt pi1: (x y: Ob) -> Hom (mul x y) x = \(x y: Ob) -> unitAbGroup pi2: (x y: Ob) -> Hom (mul x y) y = \(x y: Ob) -> unitAbGroup inl: (x y: Ob) -> Hom x (mul x y) = \(x y: Ob) -> unitAbGroup inr: (x y: Ob) -> Hom y (mul x y) = \(x y: Ob) -> unitAbGroup -- Category of Abelian Groups Ab: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = abgroup Hom (A B: Ob): U = abgrouphom A B id (A: Ob): Hom A A = idmonoidhom (A.1, A.2.1.1) c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = monoidhomcomp (A.1, A.2.1.1) (B.1, B.2.1.1) (C.1, C.2.1.1) f g HomSet (A B: Ob): isSet (Hom A B) = setmonoidhom (A.1,A.2.1.1) (B.1,B.2.1.1) L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = lemma_idmonoidhom0 (A.1, A.2.1.1) (B.1, B.2.1.1) f R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = lemma_idmonoidhom1 (A.1, A.2.1.1) (B.1, B.2.1.1) 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)) = lemma_monoidcomp0(A.1,A.2.1.1)(B.1,B.2.1.1)(C.1,C.2.1.1)(D.1,D.2.1.1)f g h -- Product Category of two Categories Product (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where x: U = carrier X y: U = carrier Y Ob: U = prod x y Hom (A B: Ob): U = prod (id x) (id y) id (A: Ob): Hom A A = (idfun x, idfun y) c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = (o x x x f.1 g.1, o y y y f.2 g.2) HomSet (A B: Ob): isSet (Hom A B) = undefined L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) 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)) = refl (Hom A D) (c A C D (c A B C f g) h) -- 3-Category with modifications between natural transformations as 3-hom morphisms modification (C D: precategory) (F G: catfunctor C D) (I J: ntrans C D F G): U = undefined Hom3Cat (X Y: precategory) (F G: catfunctor X Y): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = ntrans X Y F G Hom (A B: Ob): U = modification X Y F G A B id (A: Ob): Hom A A = undefined c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = undefined HomSet (A B: Ob): isSet (Hom A B) = undefined L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined 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)) = undefined Bicategory (X Y: precategory): precategory = Product Cat (Func X Y) Tricategory (X Y: precategory) (F G: catfunctor X Y): precategory = Product (Bicategory X Y) (Hom3Cat X Y F G) bifunctor (C D E: precategory): U = catfunctor (Product C D) E opx (L A R B: precategory) (F: catfunctor L A) (G: catfunctor R B) : catfunctor (Product L R) (Product A B) = undefined Bicategory : U = (Ob: U) * (Hom: (A B: Ob) -> precategory) * (id: (A: Ob) -> catfunctor unitCat (Hom A A)) * (c: (A B C: Ob) -> catfunctor (Product (Hom B C) (Hom A B)) (Hom A C)) * (c2: (A B C: Ob) (L R: precategory) -> catfunctor L (Hom B C) -> catfunctor R (Hom A B) -> catfunctor (Product L R) (Hom A C)) * unit Cat2 : U = (Ob: U) * (Hom: (A B: Ob) -> U) * (Hom2: (A B: Ob) -> (C F: Hom A B) -> U) * (id: (A: Ob) -> Hom A A) * (id2: (A: Ob) -> (B: Hom A A) -> Hom2 A A B B) * (c: (A B C: Ob) (f: Hom A B) (g: Hom B C) -> Hom A C) * (c2: (A B: Ob) (X Y Z: Hom A B) (f: Hom2 A B X Y) (g: Hom2 A B Y Z) -> Hom2 A B X Z) * unit --- ... Cat2Impl1 : Cat2 = ( {- Ob -} Cat.1.1, {- Hom -} \ (X Y: Cat.1.1) -> (Func X Y).1.1, {- Hom2 -} \ (X Y: Cat.1.1) -> (Func X Y).1.2, {- id -} Cat.2.1, {- id2 -} \ (A: Cat.1.1) -> (Func A A).2.1, {- c -} Cat.2.2.1, {- c2 -} \ (X Y: Cat.1.1) -> (Func X Y).2.2.1, tt ) -- ... Functions (X Y: U) (Z: isSet Y): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = X -> Y Hom (A B: Ob): U = id (X -> Y) id (A: Ob): Hom A A = idfun (X -> Y) c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = \(a:X->Y)->\(x:X)->(g(f(a)))x HomSet (A B: Ob): isSet (Hom A B) = setFun Ob Ob (setFun X Y Z) L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) 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)) = refl (Hom A D) (c A C D (c A B C f g) h) reduce (AC BC AB: precategory) (H: bifunctor BC AB AC) (L: precategory) (F: catfunctor L BC) (R: precategory) (G: catfunctor R AB) : bifunctor L R AC = compFunctor (Product L R) (Product BC AB) AC (opx L BC R AB F G) H c2impl (Ob: U) (Hom: (A B: Ob) -> precategory) (c: (A B C: Ob) -> bifunctor (Hom B C) (Hom A B) (Hom A C)) (A B C: Ob) (L R: precategory) (F: catfunctor L (Hom B C)) (G: catfunctor R (Hom A B)) : bifunctor L R (Hom A C) = reduce (Hom A C) (Hom B C) (Hom A B) (c A B C) L F R G