Type-theoretic category theory


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


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


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.} \]


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


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*} \]


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.