- What is a Category ($C$)?
- Structured Sets as Categories
- Categories of Structured Sets
- Categories of Types and Terms in Type Theory
- Categories of Categories
- Size of Categories
- Representable Functor
We can think of category theory as a generalized set theory, where in set theory we have sets and $\in$, but in category theory we have objects and arrows, where arrows are just any kinds of mappings.
So we have a kind of composition structure, where ther order of composition doesn’t matter, but the configuration matters.
And rather than reasoning structurally like PL does, it reasons “behaviorally”.
What is a Category ($C$)?
- Object collections $C_0$,
- Morphisms: Arrow collection or $hom(C)$,
- We write to say $f$ is a morphism from $a$ to $b$.
- We write $hom_C(a,b)$ to denote all morphisms from $a$ to $b$, which is also called the hom-class of all morphisms from $a$ to $b$.
- Note that $hom(C)$ is a collection of all $homs$ expanded.
- Boundary maps. domain: , codomain: ,
- Identity morphism: , which is also called loop endomorphism.
- Composition laws
- Unit laws:
- Associativity law: . From $A$ to $B$ to $C$ to $D$ we call it a path.
- If , we say the $f$ and $g$ arrows are parallel.
- Diagram: If we treat objects as vertices and arrows as directed edges, we have a directed graph
- A comutative diagram is one such that all directed paths with the same starting and end points lead to the same result.
- Whiskering: If we have a diagram that commutes, and we add one more arrow into it, we still have commuting diagram.
- Pasting: If we two diagrams, both commute, and they have a common path, then we can “stick” those two diagrams along that path, and the resulting diagram still commutes.
Structured Sets as Categories
We can construct a category from a set.
- Empty Category: $0$, which has no obejcts at all.
- Singleton Category: $1$, which has only one object, and one morphism, which is the $id$ for the object itself.
- Discrete Category: For a set $S’$, we construct a category $S$, where the objects are just the elements of the set, $S_0:=S’$, and the mophisms are only the $id$ for each object, .
Preorder Category: For a preordered set ($P’,\leq$) (a set with a reflexive and transitive binary relation on it), a category $P$ with
So the simplest category satisfying above requirements is call Interval Category ($I$), where there are only two objects, two $id$ rules, and one arrow from one to the other.
- Monoid Category: For a monoid ()
(a set $M’$, an associative binary operation $*$,
and a unit for the operation $\varepsilon$), the category $M$ with
- An example monoid is ()
Categories of Structured Sets
Some math background: According to Russell’s Paradox, we cannot have a set of all sets, but we can have category of all sets. A class is a collection of sets (or other mathematical objects) that can be unambiguously defined by a property that all its members share. A class that is not a set is called a proper class, and a class that is a set is sometimes called a small class.
- Category of sets $SET$, where objects are just sets and arrows are functions
- Category of preordered sets $PREORD$, where objects are the preordered sets, and arrows are monotone maps (functions that preserve the order).
- Category of monoids $MON$
- objects: monoids
- arrows: monoid homomorphisms (structure preserving maps of monoids)
Categories of Types and Terms in Type Theory
- objects: interpretations of types or typing context, or
- “baby tyep theory” simple example:
Categories of Categories
- What is the morphism of categories? We define functor: For categories $C,D$,
functor $F$ from $C$ to $D$ is:
- a map
- a map such that it
- respects boundaries:
- preserve identity morphisms:
- preserve composition morphisms:
- identity functors and functor composition are just as expected
Size of Categories
- a collection is either a $proper\ class$, which is $large$, or a $set$, which is $small$.
- $C\ a\ small\ category\ if\ C_1\ is\ small$, meaning $C_1\ is\ a\ set$ (which implies that $C_0\ is\ small$ because of the identity rule: $C_1$ is at least the same size of $C_0$)
- $CAT$: Category of small categories, note: $CAT\notin CAT_0$
- A category is $locally\ small$ means all homs are $small$:
A representable functor is a functor of a special form that map a locally small category into the category of sets, namely $SET$.
For a category $C$, if we fix an object in category $C$, $X:C$, we can define a functor denoted $F$ or $hom(X\rightarrow -)$:
$X$ is known as the representitive of the representable functor $F$.
To proof $F$ is a functor, we need to proof:
Proofs are skipped ;)