Axiom:Axioms for Morphisms-Only Category Theory

From ProofWiki
Jump to navigation Jump to search


Let $\mathcal{MOCT}$ be the language of (morphisms-only) category theory.

Then (morphisms-only) category theory is the mathematical theory arising from the following axioms:

\((MOCT0)\)   $:$     \(\ds \forall x,y,z,z':\) \(\ds \left({R_\circ \left({x, y, z}\right) \land R_\circ \left({x, y, z'}\right)}\right) \implies z = z' \)             $\circ$ is a partial mapping in two variables
\((MOCT1)\)   $:$     \(\ds \forall x,y:\) \(\ds \operatorname{dom} x = \operatorname{cod} y \iff \exists z: R_\circ \left({x, y, z}\right) \)             domain of composition $\circ$
\((MOCT2)\)   $:$     \(\ds \forall x,y,z:\) \(\ds R_\circ \left({x, y, z}\right) \implies \left({\operatorname{dom} z = \operatorname{dom} y \land \operatorname{cod} z = \operatorname{cod} x}\right) \)             Domain and codomain of a composite $z = x \circ y$
\((MOCT3)\)   $:$     \(\ds \forall x,y,z,a,b:\) \(\ds R_\circ \left({x, y, a}\right) \land R_\circ \left({y, z, b}\right) \implies \left({\exists w: R_\circ \left({x, b, w}\right) \land R_\circ \left({a, z, w}\right)}\right) \)             $\circ$ is associative
\((MOCT4)\)   $:$     \(\ds \forall x:\) \(\ds R_\circ \left({x, \operatorname{dom} x, x}\right) \land R_\circ \left({\operatorname{cod} x, x, x}\right) \)             Left-identity and right-identity for $\circ$

Also see