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