CATEGORY

# category

Category package contains basic notion of categories, constructions and examples.

# Basics

## Monoidal Structure

(Category Signature). The signature of category is a where could be any universe. The projection is called and projection is called , where .

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

## Precategory

Precategory defined as set of where are objects defined by its arrows . Properfies of left and right units included with composition c and its associativity.

(Precategory). More formal, precategory consists of the following. (i) A type , whose elements are called objects; (ii) for each , a set , whose elements are called arrows or morphisms. (iii) For each , a morphism , called the identity morphism. (iv) For each , a function called composition, and denoted . (v) For each and , and . (vi) For each and , , , .

(Small Category). If for all the 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 is carrier and for 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

(Initial Object). Is such object , that .

(Terminal Object). Is such object , that .

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

(Category Functor). Let and be precategories. A functor consists of: (i) A function ; (ii) for each , a function ; (iii) for each , ; (iv) for and and , .

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

(Natural Transformation). For functors , a nagtural transformation consists of: (i) for each , a morphism ; (ii) for each and , .

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

(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 is an iso if there is a morphism such that and . "f is iso" is a mere proposition.

If A is a precategory and , then (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

(Category Product).

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

## Opposite Category

(Opposite Category). The opposite category to category is a category 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

(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

(Unit Category). In unit category both and .

unitCat: precategory 

# Examples

## Category of Sets

(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

(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

(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

(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