category

Category package contains basic notion of $(\infty,1)$-categories, canstructions and examples.

Basics

Monoidal Structure

Definition (Category Signature). The signature of category is a $\Sigma_{A:U}A \rightarrow A \rightarrow U$ where $U$ could be any universe. The $pr_1$ projection is called $Ob$ and $pr_2$ projection is called $Hom(a,b)$, where $a,b:Ob$.

cat: U = (A: U) * (A -> A -> U)

Precategory

Precategory $C$ defined as set of $Hom_C(a,b)$ where $a,b:Ob_C$ are objects defined by its $id$ arrows $Hom_C(x,x)$. Properfies of left and right units included with composition c and its associativity.

Definition (Precategory). More formal, precategory $C$ consists of the following. (i) A type $Ob_C$, whose elements are called objects; (ii) for each $a,b: Ob_C$, a set $Hom_C(a,b)$, whose elements are called arrows or morphisms. (iii) For each $a: Ob_C$, a morphism $1_a : Hom_C(a,a)$, called the identity morphism. (iv) For each $a,b,c: Ob_C$, a function $Hom_C(b,c) \rightarrow Hom_C(a,b) \rightarrow Hom_C(a,c)$ called composition, and denoted $g \circ f$. (v) For each $a,b: Ob_C$ and $f: Hom_C(a,b)$, $f = 1_b \circ f$ and $f = f \circ 1_a$. (vi) For each $a,b,c,d: A$ and $f: Hom_C(a,b)$, $g: Hom_C(b,c)$, $h: Hom_C(c,d)$, $h \circ (g \circ f ) = (h \circ g) \circ f$.

Definition (Small Category). If for all $a,b: Ob$ the $Hom_C(a,b)$ forms a Set, then such category is called small category.

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))) precategory: U = (C: cat) * isPrecategory C

Accessors of the precategory structure. For $Ob$ is carrier and for $Hom$ is hom.

carrier (C: precategory): U = C.1.1 hom (C: precategory) (a b: carrier C): U = C.1.2 a b path (C: precategory) (x: carrier C): hom C x x = C.2.1 x 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

(Co)-Terminal Objects

Definition (Initial Object). Is such object $Ob_C$, that $\Pi_{x,y:Ob_C} isContr(Hom_C(x,y))$.

Definition (Terminal Object). Is such object $Ob_C$, that $\Pi_{x,y:Ob_C} isContr(Hom_C(y,x))$.

isInitial (C: precategory) (x: carrier C): U = (y: carrier C) -> isContr (hom C x y) isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) initial (C: precategory): U = (x: carrier C) * isInitial C x terminal (C: precategory): U = (y: carrier C) * isTerminal C y

Functor

Definition (Category Functor). Let $A$ and $B$ be precategories. A functor $F : A \rightarrow B$ consists of: (i) A function $F_{Ob}: Ob_hA \rightarrow Ob_B$; (ii) for each $a,b:Ob_A$, a function $F_{Hom}:Hom_A(a,b)\rightarrow Hom_B(F_{Ob}(a),F_{Ob}(b))$; (iii) for each $a:Ob_A$, $F_{Ob}(1_a) = 1_{F_{Ob}}(a)$; (iv) for $a,b,c:Ob_A$ and $f: Hom_A(a,b)$ and $g: Hom_A(b,c)$, $F(g\circ f) = F_{Hom}(g)\circ F_{Hom}(f)$.

catfunctor (A B: precategory): U = (ob: carrier A -> carrier B) * (mor: (x y: carrier A) -> hom A x y -> hom B (ob x) (ob y)) * (id: (x: carrier A) -> Path (hom B (ob x) (ob x)) (mor x x (path A x)) (path B (ob x))) * ((x y z: carrier A) -> (f: hom A x y) -> (g: hom A y z) -> Path (hom B (ob x) (ob z)) (mor x z (compose A x y z f g)) (compose B (ob x) (ob y) (ob z) (mor x y f) (mor y z g)))

Natural Transformation

Definition (Natural Transformation). For functors $F,G: C \rightarrow D$, a nagtural transformation $\gamma: F \rightarrow G$ consists of: (i) for each $x:C$, a morphism $\gamma_a : Hom_D(F(x),G(x))$; (ii) for each $x,y:C$ and $f: Hom_C(x,y)$, $G(f)\circ \gamma_x = \gamma_y \circ F(g)$.

isNaturalTrans (C D: precategory) (F G: catfunctor C D) (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)): U = (x y: carrier C) (h: hom C x y) -> Path (hom D (F.1 x) (G.1 y)) (compose D (F.1 x) (F.1 y) (G.1 y) (F.2.1 x y h) (eta y)) (compose D (F.1 x) (G.1 x) (G.1 y) (eta x) (G.2.1 x y h)) ntrans (C D: precategory) (F G: catfunctor C D): U = (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)) * (isNaturalTrans C D F G eta)

Kan Extensions

Definition (Kan Extension).

extension (C C' D: precategory) (K: catfunctor C C') (G: catfunctor C D) : U = (F: catfunctor C' D) * (ntrans C D (compFunctor C C' D K F) G)

Category Isomorphism

Definition (Category Isomorphism). A morphism $f : Hom_A(a,b)$ is an iso if there is a morphism $g: Hom_A(b,a)$ such that $1_a =_\eta g \circ f$ and $f \circ g =_\epsilon 1_b = g$. "f is iso" is a mere proposition.

If A is a precategory and $a,b: A$, then $a = b \rightarrow iso_A(a,b)$ (idtoiso).

iso (C: precategory) (A B: carrier C): U = (f: hom C A B) * (g: hom C B A) * (eta: 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))

Rezk-completion

Definition (Category). A category is a precategory such that for all $a:Ob_C$, the $\Pi_{A:Ob_C} isContr \Sigma_{B:Ob_C} iso_C(A,B)$.

isCategory (C: precategory): U = (A: carrier C) -> isContr ((B: carrier C) * iso C A B) category: U = (C: precategory) * isCategory C

Constructions

(Co)-Product of Categories

Definition (Category Product).

Product (X Y: precategory) : precategory Coproduct (X Y: precategory) : precategory

Opposite Category

Definition (Opposite Category). The opposite category to category $C$ is a category $C^{op}$ with same structure, except all arrows are inverted.

opCat (P: precategory): precategory

(Co)-Slice Category

Definition (Slice Category).

Definition (Coslice Category).

sliceCat (C D: precategory) (a: carrier (opCat C)) (F: catfunctor D (opCat C)) : precategory = cosliceCat (opCat C) D a F cosliceCat (C D: precategory) (a: carrier C) (F: catfunctor D C) : precategory

Universal Mapping Property

Definition (Universal Mapping Property).

initArr (C D: precategory) (a: carrier C) (F: catfunctor D C): U = initial (cosliceCat C D a F) termArr (C D: precategory) (a: carrier (opCat C)) (F: catfunctor D (opCat C)): U = terminal (sliceCat C D a F)

Unit Category

Definition (Unit Category). In unit category both $Ob = \top$ and $Hom = \top$.

unitCat: precategory

Examples

Category of Sets

Definition (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))

Category of Functions

Definition (Category of Functions over Sets).

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 = idfun (X -> Y) 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 = 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

Category of Categories

Definition (Category of Categories).

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

Category of Functors

Definition (Category of Functors).

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

Higher Categories

k-morphisms

Definition ($k$-Morphism). The k-morphism is defined as morphism between $(k-1)$-morphism. The base of induction, the $0$-morphism is defined as object of $1$-category, which is precategory.

equiv: U functor (C D: cat): U ntrans (C D: cat) (F G: functor C D): U modification (C D: cat) (F G: functor C D) (I J: ntrans C D F G): U ...

2-Category

Definition (2-Category).

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) ...

3-Category

Definition (3-Category).

Cat2 : U = (Ob: U) * (Hom: (A B: Ob) -> U) * (Hom2: (A B: Ob) -> (C F: Hom A B) -> U) * (Hom3: (A B: Ob) -> (C F: Hom A B) -> (F G: Hom2 A B C F) -> U) ..