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

# Category

<https://en.wikipedia.org/wiki/Category_(mathematics>) <https://ncatlab.org/nlab/show/category> <https://ncatlab.org/nlab/show/category+theory>

A category consists of

* a collection of objects
* a collection of morphisms between those objects
* each object `A` must have an identity arrow `1ᴀ`

Some authors define/enhance the identity arrow by stating that:

...such that for all morphisms `f : A → B` it holds that `f ◦ 1ᴀ = f`.

...such that for each object `A` there exists an identity morphism `1ᴀ` such that for all morphisms `f : A → B` we have `f ◦ 1ᴀ = f = 1ʙ ◦ f`

But what about a category that has no arrows between its objects \[?] Perhaps then `A = B` and `f = 1ᴀ`? Do we need the condition at all?

* We write `f : A → B` for a morphism `f` going from object `A` to `B`.
* Morphisms are closed under composition: if there is a morphism `f : A → B` and a morphism `g : B → C`, then there must be a morphism obtained by the composition, `g ◦ f : A → C`.
* As always, composition (of arrows) is associative: `f ◦ (g ◦ h) = (f ◦ g) ◦ h`

## Definition

A category is a collection of objects together with morphisms connecting these objects.

A category `C` is given by a collection `C₀` of objects and a collection `C₁` of arrows, which have the following structure:

* each arrow has an object as source and target, `f: A -> B`
* identity: each object has identity arrow, `1ₐ` or `Iₐ`
* transitivity axiom: if there is an arrow `a -> b` and an arrow `b -> c` then there must be an arrow `a -> c`

## Examples of categories

* Ordered categories: sets and relations
* Category of sets and functions
* `Hask` quasi-category of Haskell types and functions

A category C is an algebraic structure consisting of a class of objects (denoted by A, B, C, etc.), and a class of arrows (denoted by f, g, h, etc.), together with three total and one partial operation.

The first two total operations are called *target* and *source*; both assign an object to an arrow. We write `f : A <- B` (pronounced "f has type A from B") to indicate that the target of the arrow `f` is `A` and the source is `B`.

The third total operation takes an object `A` to an arrow `idᴀ : A <- A`, called the *identity* arrow on `A`.

The partial operation is called *composition* and takes two arrows to another one. The composition `f ∘ g` (read "f after g") is defined iff `f : A <- B` and `g : B <- C` for some objects A, B, C, in which case `f ∘ g : A <- C`. In other words, if the source of `f` is the target of `g`, then `f ∘ g` is an arrow whose target is the target of `f` and whose source is the source of `g`.

Composition is required to be associative and to have identity arrows as units:

∀fgh. (f: A <- B) ∧ (g: B <- C) ∧ (h: C <- D) .\
f ∘ (g ∘ h) = (f ∘ g) ∘ h = f ∘ g ∘ h

∀f. f: A <- B .\
idᴀ ∘ f = f = f ∘ idʙ