# Category Theory

[https://en.wikipedia.org/wiki/Category\_theory](https://en.wikipedia.org/wiki/Category_theory) [https://ncatlab.org/nlab/show/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
