# Type-theoretic category theory

## Semigroup

A semigroup $$g$$ has an object type $$a = Ob~g$$ and a closed associative binary operation $$bop~g : a \to a \to a$$: $\frac{(\cdot) = bop~g\quad x:Ob~g\quad y:Ob~g\quad z:Ob~g}{x \cdot (y \cdot z) = (x \cdot y) \cdot z.}$

A partial semigroup $$h$$ is a semigroup whose operation is partial: $$bop~h:a\nrightarrow a \nrightarrow a$$ where $$a = Ob~h$$.

## Monoid

A monoid $$g$$ is a semigroup with predicate $$idel~g$$ such that $\frac{idel~g~e\quad (\cdot) = bop~g\quad x:Ob~g}{e \cdot x = x\quad x \cdot e = x}$ where such $$e$$ is called an identity element of $$g$$.

## Group

A group $$g$$ is a monoid with inverse relation $$inv~g$$ such that every object in the group has an inverse and $\frac{(\cdot)=bop~g\quad x:Ob~g\quad inv~g~x~y\quad idel~g~e}{x \cdot y = e\quad y \cdot x = e.}$

## Semicategory

A semicategory $$g$$ has an object type $$Ob~g$$ and a morphism partial semigroup $$h = mor~g$$ where $$Ob~h$$ is the type of the morphisms of $$g$$ and $$bop~h$$ is morphism composition satisfying $\frac{h=mor~g\quad (\cdot) = bop~h\quad m:Ob~h\quad x=src~m\quad y=tar~m}{idm:Ob~g\to Ob~h\quad idm~y \cdot m = m \cdot idm~x}$ where $$idm~x$$ is the identity morphism on the object $$x$$, $$src~m$$ is the source object of the morphism $$m$$, and $$tar~m$$ is the target object of the morphism $$m$$. The composition, source, and target is related: $\frac{x = y \cdot z}{src~x = src~z\quad tar~x = tar~y\quad src~y = tar~z.}$

In this document, the notation $$a \to b$$ means the type of functions from $$a$$ to $$b$$, and never means a morphism from $$a$$ to $$b$$.

## Category

A category $$g$$ is a semicategory but with $$mor~g$$ a partial group instead of a partial semigroup.

### Example: a category of sets

Let $$set$$ be a category defined as follows: $$Ob~set$$ is inhabited by sets, $$Ob~(mor~set)$$ is inhabited by functions, and the morphism composition is function composition: $bop~(mor~set)~x~y = \{ (u,w) ~|~ (u,v) \in x,\ (v,w)\in y \}.$

The following are two example objects in the category of sets: \begin{align*} \{0,1,2\} &: Ob~set \\ \{a,b\} &: Ob~set \end{align*} and the following are two example morphisms from the first object to the second object: \begin{align*} \{(0,a),(1,a),(2,a)\} &: Ob~(mor~set) \\ \{(0,a),(1,a),(2,b)\} &: Ob~(mor~set). \end{align*}

## Opposite categories

The category $$op~c$$ (the opposite of the category $$c$$) is $$c$$ but with morphisms reversed.

\begin{align*} Ob~(op~c) &= Ob~c \\ Ob~(mor~(op~c)) &= Ob~(mor~c) \\ bop~(mor~(op~c))~x~y &= bop~(mor~c)~y~x \end{align*}

## Functors

A functor $$f : Functor~c~d$$ (a functor from category $$c$$ to $$d$$) consists of two functions $$fo$$ and $$fm$$: \begin{align*} fo~f &: Ob~c \to Ob~d \\ fm~f &: Ob~(mor~c) \to Ob~(mor~d) \end{align*} satisfying $\frac{f:Functor~c~d\quad x : Ob~c\quad pure=fo~f\quad map=fm~f}{map~(idm~x) = idm~(pure~x)}$ and $\frac{f:Functor~c~d \quad map=fm~f\quad (\cdot)=bop~c \quad (\bullet)=bop~d}{map~(m\cdot n)=map~m\bullet map~n.}$

Much could be written, but the most important thing is that you get the idea.