> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/450-category-theory/terms/category-theory.md).

# Category Theory

<https://en.wikipedia.org/wiki/Category_theory> <https://ncatlab.org/nlab/show/category+theory>

Category theory 1. Idea 2. The central constructions Presheaves Universal constructions 3. The central theorems 4. Applications In pure mathematics Outside of mathematics 5. Contrast to theories of other objects Category theory vs. set theory Category theory vs. order theory 6. Theorems 7. Related concepts 8. References History Basic category theory Topos theory Higher category theory Foundations

## Category theory introduction

Category

* A generalisation of a graph (transitive closure)
* Nodes are called objects: a, b, c, …
* Arrows between objects are called morphisms: f :: a -> b

Arrows are composable:

* f :: a -> b,
* g :: b -> c,
* g ∘ f :: a -> c (exists if the previous two exist)

Identity arrows (always exist!):

* ida :: a -> a,
* id ○ f = f,
* g ○ id = g

𝗦𝗲𝘁 category is a category in which:

* Objects are sets
* Arrows are functions
* *Initial Object*: there is a unique arrow from initial object to any other object

Initial Object in Set

* Empty set ∅
* Unique function from `⌀ -> a`
* `absurd :: Void -> a`
* `Void` is the uninhabited type
* *Terminal Object*: there is a unique arrow from any object to terminal object

Terminal Object in Set

* Singleton set
* Unique function: for every element of set `a` return the single element of the singleton set
* Unit type `()` with one element `()`
* `unit :: a -> ()`
* `unit _ -> ()`

**Universal Construction** is used to "pick" objects in a category. Because we cannot examine the internals of objects, the only way we can derive info about them is exploring how they relate to each other via arrows.

* Product (Elimination)
  * `c` is a product of `a` and `b`
  * Two arrows `p` and `q` (projections)

    c :: (a, b)

    p (a, b) = a

    q (a, b) = b
  * In set theory, product is a cartesian product, i.e. a pair of elements
  * In logic: ∧ (conjunction elimination)

    a ∧ b           a ∧ b

    &#x20; a               b

Using universal construction, we fix the objects `a` and `b` in the attempt to find their product, an object `c`. In order for `c` to be a product of `a` and `b`, there must be two projection functions, `c -> a` and `c -> b`.

## Category Theory

Category theory formalizes *mathematical structure* and its concepts in terms of a *labeled directed graph* called a **category**, whose nodes are called **objects**, and whose labelled directed edges are called **arrows** or **morphisms**.

A category has two basic properties:

* the ability to compose the arrows associatively
* the existence of an identity arrow for each object