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