```
open import Agda.Primitive using (Level; _β_; lsuc; lzero)
open import Types.product
open import Types.relations
open import Types.equality
module Category.category where
```

A category is the object of study in category theory. It can be thought of being a bunch of objects, which are associated by a bunch of arrows between those objects, with the arrows being composable and each object having unit arrows. This minimal structure ensures a multitude of object types studied in mathematics can fit the description.

A category β consists of:

- A collection of objects \(x \in obj(β)\)
- A collection of morphisms between those objects \(hom(π) = \{ f : a β b : a,b β β \}\), called a βhomβ set

such that:

- Morphisms compose:

If \[f : a β b, g : b β c\] then \[g β f : a β c\]

- Morphisms are associative:

\[If~~ f : a β b,~ g : b β c ~~and~~ h : c β d ~~then~~ h β (g β f) = (h β g) β f\]

- Morphisms have identities: For every object x, there exists a morphism \(1β : x β x\) called the identity morphism for x, such that for every morphism \(f : a β x\) and every morphism \(g : x β b\), we have \(1β β f = f\) and \(g β 1β = g\).

```
record Category (o β e : Level) : Set (suc (o β β β e)) where
infix 4 _β_ _β_
infixr 9 _β_
field
: Set o -- objects
Obj _β_ : Rel Obj β -- morphism
_β_ : β {A B} β Rel (A β B) e -- equivalence of morphisms
: β {A} β (A β A) -- identity
id
-- composition of morphisms
_β_ : β {A B C} β (B β C) β (A β B) β (A β C)
-- laws
-- satisfy associativity
: β {A B C D} {f : A β B} {g : B β C} {h : C β D} β (h β g) β f β h β (g β f)
assoc -- satisfy identity
: β {A B} {f : A β B} β id β f β f
identityΛ‘ : β {A B} {f : A β B} β f β id β f
identityΚ³ -- has an equivalence for morphisms
: β {A B} β IsEquivalence (_β_ {A} {B})
equiv -- composition is congruent on equivalence
: β {A B C} {f h : B β C} {g i : A β B} β f β h β g β i β f β g β h β i β-resp-β
```

The machinery of category theory also admits a duality, like an object and its mirror image. The opposite or dual of a category \(β\), denoted by \(βα΄Όα΅\), is the same category, but with all morphisms in the opposite direction. All laws and machinery of category theory have their dual versions.

```
record Categoryα΄Όα΅ (o β e : Level) : Set (suc (o β β β e)) where
infix 4 _β_ _β_
infixr 9 _β_
field
: Set o -- objects
Obj _β_ : Rel Obj β -- morphism
_β_ : β {A B} β Rel (B β A) e -- equivalence of morphisms
: β {A} β (A β A) -- identity
id
-- composition of morphisms
_β_ : β {A B C} β (B β A) β (C β B) β (C β A)
-- laws
-- satisfy associativity
: β {A B C D} {f : A β B} {g : B β C} {h : C β D} β h β (g β f) β (h β g) β f
assoc -- satisfy identity
: β {A B} {f : A β B} β id β f β f
identityΛ‘ : β {A B} {f : A β B} β f β id β f
identityΚ³ -- has an equivalence for morphisms
: β {A B} β IsEquivalence (_β_ {A} {B})
equiv -- composition is congruent on equivalence
: β {A B C} {f h : B β C} {g i : A β B} β g β i β f β h β g β f β i β h β-resp-β
```

We can use various mathematical structures to construct categories out of. When defining a category, we have to decide what our objects and our morphisms would be and how would the morphisms compose. This decision has to be taken in a way that the conditions of being a category are satisfied (associativity, identity). We would then have a category of our chosen object.

A category of sets is the simplest of categories we can construct and the most intuitive to understand given we have been trained to think in terms of sets.

- Objects: Sets
- Morphisms: Total functions between sets
- Composition: Function composition

- Objects: Groups
- Morphisms: Group homomorphisms
- Composition: Composition of group homomorphisms

- Objects: Rings
- Morphisms: Ring homomorphisms
- Composition: Composition of ring homomorphisms

- Objects: Topological Spaces
- Morphisms: Continuous maps/functions between spaces
- Composition: Composition of continuous maps

Here are some other examples:

Category | Objects | Morphisms |
---|---|---|

Set | sets | total functions |

Group | groups | group homomorphisms |

Top | topological spaces | continuous functions |

Vectβ | vector spaces over field K | linear transformations |

Poset | partially ordered sets | order-preserving functions |

TopVect | topological vector spaces | continuous linear maps |

π | differentiable manifolds | differentiable maps |

Banach spaces | open subsets of Banach spaces | differentiable maps |

π | vector bundles | vector bundle maps |

There are in fact infinitely many more and so we are going to move along now.

Before explaining higher categories, let us look at a structure from algebraic topology called simplexes and simplicial complexes.

A simplex is an n-dimensional βtriangleβ. Some examples of the first few dimensional simplices are:

- 0-simplex: point
- 1-simplex: line segment
- 2-simplex: triangle
- 3-simplex: tetrahedron

An n-dimensional simplex is also called an **(n+1)-cell**.

A simplicial complex is a structure formed by gluing together a bunch of simplices. The gluing process has to follow a set of properties:

A set of simplices \(\mathcal{K}\) is a simplicial complex if: - Every face of a simplex from \(\mathcal{K}\) is also in \(\mathcal{K}\) - Intersections of any two simplices is a face of both the simplices

A simplicial complex is of dimension n if the largest dimension of all the constituent simplices is n.

\[ dim(\mathcal{K}) = max(dim(Ο_i)) \]

Examples:

- Any n-ary tree is a simplicial complex
- An undirected acyclic graph is a 1-dimensional simplicial complex
- Any 1-D simplicial complex is a hypergraph
- Any n-dimensional convex hull is a simplicial complex
- Nerves of any category are simplicial complex
- The triangulation of a polygon in the plane is a simplicial complex

Simplicial complexes can be used to create or represent topological spaces and serve as a very useful tool. They can also be used to formalize algebraic constraints in geometric terms as well.

The Nerve N(β) of a category β is a simplicial complex constructed from objects as vertices of simplices and morphisms of β as the edges.

Given two (or more) categories, their cartesian product is also a category.

Given two categories β and π», their product is a category with: - Pairs (C, D) as objects such that C β β and D β π» - (f, g) as morphisms where - \(f : C_1 β C_2; C_i β β\) - \(g : D_1 β D_2; D_i β π»\) - composition of morphisms defined as \((f_1, g_1) β (f_2, g_2) = (f_1 β f_2, g_1 β g_2)\) - identities defined as \(1_{(C, D)} = (1_C, 1_D)\)

Free categories are a result of using a general pattern called βfree constructionsβ for building categories. The idea of free objects in mathematics can be related to all types of objects with algebraic structure, and provides a general method of constructing objects using a set of βconstructorβ objects. The process of construction proceeds as follows:

- Take a set of objects to construct the free category with
- Construct all possible combinations of these objects, in other words, the power set of the set of those objects. These form the algebraic object of interest
- Define relations between every pair of objects according to the kind of algebraic object to construct

For free categories these rules become:

- Consider a bunch of objects to be taken as generators
- Construct the power set of these generators, these form the objects of the free category
- Define morphisms between every pair of objects and all compositions of their morphisms, together they form the hom-set of the free category