Double Categories
Definitions
Definitions
Definition 1 (Category) A Category \(C\) consists of the following data:
First class \(C_0\) and another set \(C_1\);
Functions \(s, t: C_1 \rightarrow C_0\) (the source and target functions);
A function \(\text{id} : C_0 \rightarrow C_1\) (the function which picks out an identity) such that \(\text{id}\) equalises \(s\) and \(t\);
For every \(f, g \in C_1\) such that \(t(f) = s(g)\) there is a unique element (there composition) \(g \circ f \in C_1\) where \(s(g\circ f) = s(f)\) and \(t(g \circ f) = t(g)\).
This data is required to satisfy:
For every \(f \in C_1\), we have that \(f \circ \text{id}(s(f)) = f\) and \(\text{id}(t(f)) \circ f = f\);
For every \(f, g, h \in C_1\), we have that \((h\circ g) \circ f = h \circ (g \circ f)\).
Definition 2 (Double Category) A Double Category \(\mathbb{C}\) consists of the following data:
a Category \(\ \mathbb{C}_0 \ \), whose objects we call 0-cells, and whose arrows we call tight 1-cells \(f: V \rightarrow V'\);
a Category \(\ \mathbb{C}_1 \ \), whose objects we call loose 1-cells \(M: V \not\rightarrow W\), and whose arrows we call 2-cells
two functors \(\text{src}, \text{tgt} : \mathbb{C}_1 \rightarrow \mathbb{C}_0\) called source and target respectively;
composition and identity functors \(\circ : \mathbb{C}_1 \times_{\mathbb{C}_0} \mathbb{C}_1 \rightarrow \mathbb{C}_1\) and \(\text{id} : \mathbb{C}_0 \rightarrow \mathbb{C}_1\);
natural families of isomorphisms in \(\mathbb{C}_1\):
These data are required to satisfy the following coherence axioms which manifest as equations between composite 2-cells.
The first of these is the following composite,
is required to be equal to this composite,
A further equation is required, which declares that the next composite
is equal to
Several questions come about when staring at the above definition. If arrows are objects in \(\mathbb{C}_1\) what gives the right to state that they look like arrows with sources and targets that could just as well be source and targets of arrows in \(\mathbb{C}_0\). The source and target functors are lacking defining equations they should be compatible with the composition and identity functors in the way that is implied from the mantra “double categories are category objects in the category of categories”. In particular, the identity functor must equalise the source and target functors meaning that enrichment is ill-defined or based on evil equality. The more significant problem is that the presentation of squares need to have a specific orientation which produces conflicts in the literature.
A better definition starts from finding a better definition for categories.
Definition 3 (Category, indexed version) A category is the data of:
A class \(C_0\);
For every \(A, B \in C_0\) a set \(C_1(A,B)\);
For every \(A \in C_0\), a distinguished element \(\text{id}_A \in C_1(A,A)\);
For every \(A, B, C \in C_0\), and every \(f \in C_1(A, B)\), as well as \(g \in C_1(B,C)\) there is a \(g \circ f \in C_1(A,C)\);
satisfying the requirements that
For every \(A, B \in C_0\), and every \(f \in C_1(A, B)\) the following equations hold
\[f \circ \text{id}_A = f = \text{id}_B \circ f.\]
For every \(A, B, C, D \in C_0\), and every \(f \in C_1(A, B)\) and also every \(g \in C_1(B,C)\) as well as \(h \in C_1(C, D)\), the following equation holds
\[(h \circ g) \circ f = h \circ (g \circ f).\]
The sets \(C_1(A,B)\) are pairwise disjoint.
It can be shown through a laborious formal argument that the two definitions, the version with source and target and the indexed version are equivalent and thus we can use the capitalised or uncapitalised interchangeably. We would like to have a similar definition for double categories as for the definition of category. The reason to do this is so that there is no confusion in the definition and data can be expressed clearly.
Definition 4 (Double category, indexed version) A double category \(\mathbb{C}\) consists of the following data:
A class of objects \(\mathcal{O}\) whose members are called the 0-cells of \(\mathbb{C}\) (generically upper roman from the beginning of the alphabet);
For every \(A, A' \in \mathcal{O}\) a set \(\text{hom}_{\tau}(A,A')\), called tight arrows (generically lower roman from the beginning of the alphabet);
For every \(A, B \in \mathcal{O}\) a set \(\text{hom}_{\lambda}(A,B)\) called loose arrows (generically lower roman from middle of the alphabet);
For every \(A \in \mathcal{O}\) a distinguished tight arrow \(1_A \in \text{hom}_{\tau}(A,A)\);
For every \(A \in \mathcal{O}\) a distinguished loose arrow \(\text{id}_A \in \text{hom}_{\lambda}(A,A)\), also written as just \(A\) if convenient;
For every \(A, A', A'' \in \mathcal{O}\), and every \(f \in \text{hom}_{\tau}(A,A')\) and also every \(f' \in \text{hom}_{\tau}(A',A'')\), there is a \(f' \circ_{\tau}f \in \text{hom}_{\tau}(A,A'')\);
For every \(A, B, A', B' \in \mathcal{O}\), and every \(f \in \text{hom}_{\tau}(A,A'), g \in \text{hom}_{\tau}(B,B')\) and also every \(p \in \text{hom}_{\lambda}(A,B), p' \in \text{hom}_{\tau}(A',B')\), there is a set \(\text{Sq}^{A,B}_{A',B'}(f, g, p, p')\) called witnesses (generically lower greek). For simplicity, we will drop identities as redundant information;
- For every \(A, B \in \mathcal{O}\), and every \(p \in \text{hom}_{\lambda}(A,B)\) there is a distinguished witness \(\upsilon_p \in \text{Sq}_{A, B}^{A,B}(p, p)\). For simplicity, if \(p = \text{id}_A\) for \(A \in \mathcal{O}\) then we will write \(\upsilon_{id_A}\) as \(\upsilon_A\);
- For every \(A, B, A', B', A'', B'' \in \mathcal{O}\), and every \(f \in \text{hom}_{\tau}(A,A'), f' \in \text{hom}_{\tau}(A',A''), g \in \text{hom}_{\tau}(B,B'), g' \in \text{hom}_{\tau}(B',B'')\) and also every \(p \in \text{hom}_{\lambda}(A,B), p' \in \text{hom}_{\lambda}(A',B'), p''\in \text{hom}_{\lambda}(A'',B'')\) as well as every \(\varphi \in \text{Sq}^{A, B}_{A', B'}(f, g, p, p'), \varphi' \in \text{Sq}^{A', B'}_{ A'', B''}(f', g', p', p'')\) there is a \(\varphi' \circ_{\tau}^2\varphi \in \text{Sq}^{A, B}_{ A'', B''}(f' \circ_{\tau}f, g' \circ_{\tau}g, p, p'')\).
For every \(A, B, C \in \mathcal{O}\) and every \(p \in \text{hom}_{\lambda}(A,B), q \in \text{hom}_{\lambda}(B,C)\) there is a \(q \circ_{\lambda}p \in \text{hom}_{\lambda}(A,C)\). For simplicity we will write \(id_B \circ_{\lambda}p\) as \(B \circ_{\lambda}p\).;
For every \(A, B, C, A', B', C' \in \mathcal{O}\) and every \(f \in \text{hom}_{\tau}(A,A'), g \in \text{hom}_{\tau}(B,B'), h \in \text{hom}_{\tau}(C,C')\) and also every \(p \in \text{hom}_{\lambda}(A,B), q \in \text{hom}_{\lambda}(B,C), p' \in \text{hom}_{\lambda}(A',B'), q' \in \text{hom}_{\lambda}(B',C')\) as well as every witness \(\varphi \in \text{Sq}^{A, B}_{A', B'}(f, g, p, p')\) and \(\psi \in \text{Sq}^{B, C}_{B', C'}(g, h, q, q')\) then there is a witness \(\psi \circ_{\lambda}^2\varphi \in \text{Sq}^{B,C}_{B',C'}(f, h, q \circ_{\lambda}p, q' \circ_{\lambda}p')\).
For every \(A, B \in \mathcal{O}\) and every \(p \in \text{hom}_{\lambda}(A,B)\) there is a witness \(\ell_p \in \text{Sq}^{A, B}_{A, B}(B \circ_{\lambda}p, p)\). The witness is natural in \(p\) in the sense that: for every \(p' \in \text{hom}_{\lambda}(A,B)\) and every \(\varphi \in \text{Sq}^{A, B}_{A, B}(p, p')\) we have
\[ \varphi \circ_{\tau}^2\ell_p = \ell_{p'} \circ_{\tau}^2(\upsilon_{B} \circ_{\lambda}^2\varphi) .\]
Each \(\ell_p\) also comes equipped with a friend \(k_p \in \text{Sq}^{A, B}_{A, B}(p, B \circ_{\lambda}p)\) such that \(k_p \circ_{\tau}^2\ell_p = \upsilon_{B \circ_{\lambda}p}\) and \(\ell_p \circ_{\tau}^2k_p = \upsilon_{p}\);
- For every \(A, B \in \mathcal{O}\) and every \(p \in \text{hom}_{\lambda}(A,B)\) there is a witness \(\rho_p \in \text{Sq}^{A, B}_{A, B}(p \circ_{\lambda}A, p)\). The witness is natural in \(p\) in the sense that: for every \(p' \in \text{hom}_{\lambda}(A,B)\) and every \(\varphi \in \text{Sq}^{A, B}_{A, B}(p, p')\) we have
\[\varphi \circ_{\tau}^2r_p = r_{p'} \circ_{\tau}^2(\varphi \circ_{\lambda}^2\upsilon_A)\]
Each \(\rho_p\) comes equipped with a friend \(\sigma_p \in \text{Sq}^{A, B}_{A, B}(p, p \circ_{\lambda}A)\) such that \(\rho_p \circ_{\tau}^2\sigma_p = \upsilon_p\) and \(\sigma_p \circ_{\tau}^2\rho_p = \upsilon_{p \circ_{\lambda}A}\);
- For every \(A, B, C, D \in \mathcal{O}\) and every \(r \in \text{hom}_{\lambda}(C,D), q \in \text{hom}_{\lambda}(B,C), p \in \text{hom}_{\lambda}(A,B)\) there is a witness \(a_{r, q, p} \in \text{Sq}^{A, D}_{A, D}((r \circ_{\lambda}q) \circ_{\lambda}p, r \circ_{\lambda}(q \circ_{\lambda}p))\). This witness is natural in \(r, q\) and \(p\) simultaneously meaning that: for every \(r' \in \text{hom}_{\lambda}(C, D), q' \in \text{hom}_{\lambda}(B, C), p' \in \text{hom}_{\lambda}(A, B)\) and every \(\psi \in \text{Sq}^{C, D}_{C, D}(r, r'), \chi \in \text{Sq}^{B, C}_{B, C}(q, q'), \varphi \in \text{Sq}^{A, B}_{A, B}(p, p')\) we have
\[a_{r', q, p}\circ_{\tau}^2((\psi \circ_{\lambda}^2\upsilon_{q}) \circ_{\lambda}^2\upsilon_{p}) = (\psi \circ_{\lambda}^2(\upsilon_{q} \circ_{\lambda}^2\upsilon_{p})) \circ_{\tau}^2a_{r, q, p}\]
\[a_{r, q', p} \circ_{\tau}^2((\upsilon_{r} \circ_{\lambda}^2\chi) \circ_{\lambda}^2\upsilon_{p}) = (\upsilon_{r} \circ_{\lambda}^2(\chi \circ_{\lambda}^2\upsilon_{q})) \circ_{\tau}^2a_{r, q, p},\]
\[ a_{r, q, p'} \circ_{\tau}^2((\upsilon_{r} \circ_{\lambda}^2\upsilon_{q}) \circ_{\lambda}^2\varphi) = (\upsilon_{r} \circ_{\lambda}^2(\upsilon_{q} \circ_{\lambda}^2\varphi)) \circ_{\tau}^2a_{r, q, p} \]
Each \(a_{r, q, p}\) comes equipped with a friend \(b_{r, q, p} \in \text{Sq}^{A, D}_{A, D}(r \circ_{\lambda}(q \circ_{\lambda}p)), (r \circ_{\lambda}q) \circ_{\lambda}p)\) such that \(a_{r,q,p} \circ_{\tau}^2b_{r, q, p} = \upsilon_{r \circ_{\lambda}(q \circ_{\lambda}p)}\) and \(b_{r, q, p} \circ_{\tau}^2a_{r, q, p} = \upsilon_{(r \circ_{\lambda}q) \circ_{\lambda}p}\).
This data is required to satisfy the following:
For every \(A, A' \in \mathcal{O}\) and every \(f \in \text{hom}_{\tau}(A,A')\) we have
\[1_{A'} \circ_{\tau}f = f = f \circ_{\tau}1_{A};\]
For every \(A, B, A', B', A'', B'', A''', B''' \in \mathcal{O}\) and every \(p \in \text{hom}_{\lambda}(A, B), p' \in \text{hom}_{\lambda}(A', B'), p'' \in \text{hom}_{\lambda}(A'', B''), p''' \in \text{hom}_{\lambda}(A''', B''')\) and also every \(f \in \text{hom}_{\tau}(A, A'), g \in \text{hom}_{\tau}(B,B'), f' \in \text{hom}_{\tau}(A', A''), g' \in \text{hom}_{\tau}(B',B''), f'' \in \text{hom}_{\tau}(A'', A'''), g'' \in \text{hom}_{\tau}(B'',B''')\) as well as \(\varphi \in \text{Sq}^{A, B}_{A', B'}(f, g, p, p'), \varphi' \in \text{Sq}^{A', B'}_{A'', B''}(f', g', p', p''), \varphi'' \in \text{Sq}^{A'', B''}_{A''', B'''}(f'', g'', p'', p''')\) we have
\[ f'' \circ_{\tau}(f' \circ_{\tau}f) = (f'' \circ_{\tau}f') \circ_{\tau}f,\]
\[ \varphi'' \circ_{\tau}^2(\varphi' \circ_{\tau}^2\varphi) = (\varphi'' \circ_{\tau}^2\varphi') \circ_{\tau}^2\varphi;\]
For every \(A, B, A', B' \in \mathcal{O}\) and every \(p \in \text{hom}_{\lambda}(A, B), p' \in \text{hom}_{\lambda}(A',B')\) and also every \(f \in \text{hom}_{\tau}(A,A'), g \in \text{hom}_{\tau}(B,B')\) as well as every witness \(\varphi \in \text{Sq}^{A, B}_{A', B'}(f, g, p, p')\) we have
\[\varphi \circ_{\tau}^2\upsilon_p = \varphi = \upsilon_{p'} \circ_{\tau}^2\varphi;\]
For every \(A, B, C, D, E \in \mathcal{O}\) and every \(s \in \text{hom}_{\lambda}(D,E), r \in \text{hom}_{\lambda}(C,D), q \in \text{hom}_{\lambda}(B, C), p \in \text{hom}_{\lambda}(A, B)\) we have
\[ ( (\upsilon_s \circ_{\lambda}^2a_{r, q, p}) \circ_{\tau}^2a_{s, r \circ_{\lambda}q, p} ) \circ_{\tau}^2(a_{s, r, q} \circ_{\lambda}^2\upsilon_p) = a_{s, r, q \circ_{\lambda}p} \circ_{\tau}^2a_{s \circ_{\lambda}r, q, p};\]
For every \(A, B, C \in \mathcal{O}\) and every \(q \in \text{hom}_{\lambda}(B, C), p \in \text{hom}_{\lambda}(A, B)\) we have
\[ (\upsilon_{p} \circ_{\lambda}^2\ell_q) \circ_{\tau}^2a_{q, B, p} = \rho_p \circ_{\lambda}^2\upsilon_{B};\]
For every \(A, B, C, A', B', C', A'', B'', C'' \in \mathcal{O}\) and \(f \in \text{hom}_{\tau}(A,A'), f' \in \text{hom}_{\tau}(A',A''), g \in \text{hom}_{\tau}(B, B'), g' \in \text{hom}_{\tau}(B',B''), h \in \text{hom}_{\tau}(C,C'), h' \in \text{hom}_{\tau}(C',C'')\) and every \(q \in \text{hom}_{\lambda}(B,C), p \in \text{hom}_{\lambda}(A,B), q' \in \text{hom}_{\lambda}(B',C'), p' \in \text{hom}_{\lambda}(A',B'), q'' \in \text{hom}_{\lambda}(B'',C''), p'' \in \text{hom}_{\lambda}(A'', B'')\) and also every \(\varphi \in \text{Sq}_{A',B'}^{A,B}(f,g,p,p'), \psi \in \text{Sq}_{B',C'}^{B,C}(g,h,q,q'), \varphi' \in \text{Sq}_{A'',B''}^{A',B'}(f',g',p', p''), \psi' \in \text{Sq}_{B'',C''}^{B',C'}(g',h',q',q'')\) we have
\[(\psi \circ_{\lambda}^2\varphi) \circ_{\tau}^2(\psi' \circ_{\lambda}^2\varphi') = (\varphi' \circ_{\tau}^2\varphi) \circ_{\lambda}^2(\psi' \circ_{\tau}^2\psi).\]
Definition 5 (Double category, 1-categorical version) A double category \(\mathbb{C}\) is the data of
A class \(\mathcal{O}\) (generically upper roman from the beginning of the alphabet);
A set \(\text{hom}_{\tau}(A,B)\) for each \(A, B \in \mathcal{O}\) (of tight morphisms, generically lower roman from the beginning of the alphabet);
A set \(\text{hom}_{\lambda}(A,B)\) for each \(A, B \in \mathcal{O}\) (of loose morphisms, generically lower roman from the middle of the alphabet);
A distinguished tight arrow \(1_A \in \text{hom}_{\tau}(A,A)\) and a distinguished loose arrow \(\text{id}_A \in \text{hom}_{\lambda}(A,A)\) for \(A \in \mathcal{O}\);
For \(f \in \text{hom}_{\tau}(A,B), f' \in \text{hom}_{\tau}(B, C)\) there is \(f' \circ_{\tau}f \in \text{hom}_{\tau}(A,C)\) for \(A, B, C \in \mathcal{O}\);
For \(p \in \text{hom}_{\lambda}(A, B), q \in \text{hom}_{\lambda}(B,C)\) there is \(q \circ_{\lambda}p \in \text{hom}_{\lambda}(A,C)\) for \(A, B, C \in \mathcal{O}\);
A set \(\text{Sq}^{A,B}_{C,D}(f,g,p,p')\) for each \(f \in \text{hom}_{\tau}(A,C), g \in \text{hom}_{\tau}(B,D)\) and \(p \in \text{hom}_{\lambda}(A,B), p' \in \text{hom}_{\lambda}(C,D)\) for \(A, B, C, D \in \mathcal{O}\) (generically lower case greek). For simplicity, we will drop any identities as redundant information;
A distinguished square \(\upsilon_p \in \text{Sq}_{A,B}^{A,B}(p,p)\) for each \(p \in\text{hom}_{\lambda}(A,B)\) and for \(A, B \in \mathcal{O}\);
For \(\phi \in \text{Sq}^{A,B}_{C,D}(f,g,p,p'), \phi' \in \text{Sq}^{C,D}_{E,F}(f',g',p',p'')\) there is \(\phi' \circ_{\tau}^2\phi \in \text{Sq}^{A,B}_{E,F}(f'\circ_{\tau}f,g' \circ_{\tau}g,p,p'')\) for \(A, B, C, D, E, F \in \mathcal{O}\);
For \(\phi \in \text{Sq}^{A,B}_{C,D}(f,g,p,p'), \psi \in \text{Sq}^{B,E}_{D,F}(g,h,q,q')\) there is \(\psi \circ_{\lambda}^2\phi \in \text{Sq}^{A,E}_{C,F}(f,h,q \circ_{\lambda}p, q' \circ_{\lambda}p')\) for \(A, B, C, D, E, F \in \mathcal{O}\);
Satisfying the following relations:
For \(A, B, C, D \in \mathcal{O}\) and \(f \in \text{hom}_{\tau}(A,B), f' \in \text{hom}_{\tau}(B, C), f'' \in \text{hom}_{\tau}(C,D)\) we have that
\[f \circ_{\tau}1_A = f = 1_B \circ_{\tau}f\]
and
\[(f'' \circ_{\tau}f') \circ_{\tau}f = f'' \circ_{\tau}(f' \circ_{\tau}f);\]
For every \(A, B, C, D \in \mathcal{O}\) and \(p \in \text{hom}_{\lambda}(A,B), q \in \text{hom}_{\lambda}(B, C), r \in \text{hom}_{\lambda}(C,D)\) we have that
\[p \circ_{\lambda}\text{id}_{A} = p = \text{id}_{B} \circ_{\lambda}p\]
and
\[(r \circ_{\lambda}q) \circ_{\lambda}p = r \circ_{\lambda}(q \circ_{\lambda}p);\]
For every \(A, B, C, D, E, F, G, H \in \mathcal{O}\) and \(\phi \in \text{Sq}^{A,B}_{C,D}(f,g,p,p'), \phi' \in \text{Sq}^{C,D}_{E,F}(f',g',p',p''), \phi'' \in \text{Sq}^{E, F}_{G, H}(f'',g'',p'', p''')\) we have that
\[\upsilon_{p'} \circ_{\tau}^2\phi = \phi = \phi \circ_{\tau}^2\upsilon_{p}\]
and
\[(\phi'' \circ_{\tau}^2\phi') \circ_{\tau}^2\phi = \phi'' \circ_{\tau}^2(\phi' \circ_{\tau}^2\phi);\]
For every \(A, B, C, D, E, F, G, H \in \mathcal{O}\) and \(\phi \in \text{Sq}^{A,B}_{C,D}(f,g,p,p'), \psi \in \text{Sq}^{B,E}_{D,F}(g,h,q,q'), \chi \in \text{Sq}^{E, G}_{F, H}(h,k,r,r')\) we have that
\[(\chi \circ_{\lambda}^2\psi) \circ_{\lambda}^2\phi = \chi \circ_{\lambda}^2(\psi \circ_{\lambda}^2\phi);\]
For every \(A, B, C, D, E, F, G, H, K \in \mathcal{O}\) and \(\phi \in \text{Sq}^{A,B}_{C,D}(f,g,p,p'), \phi' \in \text{Sq}^{C,D}_{E,F}(f',g',p',p''), \psi \in \text{Sq}^{B, G}_{D, H}(g, h, q, q'), \psi' \in \text{Sq}^{D, H}_{F, K}(g', h', q', q'')\) we have that
\[(\phi' \circ_{\tau}^2\phi) \circ_{\lambda}^2(\psi' \circ_{\tau}^2\psi) = (\phi' \circ_{\lambda}^2\psi') \circ_{\tau}^2(\phi \circ_{\lambda}^2\psi).\]
Let \(\mathcal{C}\text{at}\) denote the category which has as objects (small) categories and morphisms as functors between these.
To produce the following definition we will need to be explicit about what the fibre products are in \(\mathcal{C}\text{at}\), namely the strict pullbacks. For three (small) categories \(C, D, E\) in \(\mathcal{C}\text{at}\) and functors \(f: C \rightarrow E\), \(g: D \rightarrow E\). The strict pullback is denoted \(C \times_E D\) and it is small category with an object set consisting
\[\text{ob}(C\times_E D) = \{(c,d) \in \text{ob}(C)\times\text{ob}(D) \ :|: \ f^o(c) = g^o(d) \}\]
and morphisms, for each \((c,d)\) and \((c',d')\)
\[(C\times_E D)((c,d),(c',d')) = \{(\varphi, \phi) \in \text{hom}_C(c, c') \times \text{hom}_D(d,d') \ :|: \ f^m(\varphi) = g^m(\phi) \in \text{hom}_E(f^o(c),g^o(d'))\} \]
Definition 6 (Double category, as a category object internal to Cat) A category object in \(\mathcal{C}\text{at}\) is the data of two (small) categories \(C_0\) and \(C_1\), and six functors, drawn in the way that is displayed in the following diagram
Satisfying the following additional axioms, expressed as commuting diagrams in \(\mathcal{C}\text{at}\):
Theorem 1 (The two 1-categorical definitions are essentially the same) A category object in \(\mathcal{C}\text{at}\) is equivalently a double category.
A double category is equivalently a category object internal to \(\mathcal{C}\text{at}\).
Proof 1. \((``\Rightarrow")\)
This is a series of definition re-writing.
\[\mathcal{O} \triangleq \text{ob}(C_0)\]
\[\forall A,B \in \mathcal{O}, \ \text{hom}_{\tau}(A,B) \triangleq C_0(A,B)\]
\[\forall A,B \in \mathcal{O}, \ \text{hom}_{\lambda}(A,B) \triangleq \{p \in \text{ob}(C_1) \ :|: \ s^o(p) = A, t^o(p) = B \}\]
\[\forall A \in \mathcal{O}, 1_A \triangleq \text{id}^{C_0}_A\]
\[\forall A \in \mathcal{O}, \text{id}_A \triangleq \text{id}^o(A)\]
\[\forall A, B, C, D \in \mathcal{O}, \forall f \in \text{hom}_{\tau}(A,C), g \in \text{hom}_{\tau}(B,D), p \in \text{hom}_{\lambda}(A,B), p' \in \text{hom}_{\lambda}(C,D)\] \[ \text{Sq}_{A,B,C,D}(f,g,p,p') \triangleq \{\varphi \in C_1(p,q) \ :|: \ s^o(p) = A, t^o(p) = B, s^m(\varphi) = f, s^o(q) = C, t^o(q) = D, t^m(\varphi) = g\}\]
\[\forall A, B \in \mathcal{O}, \forall p \in \text{hom}_{\lambda}(A,B), \upsilon_p \triangleq \text{id}^{C_1}_p\]
\[\forall A, B, C \in \mathcal{O}, \forall f \in \text{hom}_{\tau}(A,B), f' \in \text{hom}_{\tau}(B,C),\] \[ f'\circ_{\tau}f \triangleq \circ^{C_0}(f',f)\]
\[\forall A, B, C \in \mathcal{O}, \forall p \in \text{hom}_{\lambda}(A,B), q \in \text{hom}_{\lambda}(B,C),\] \[ q\circ_{\lambda}p \triangleq \ \text{comp}^o((q,p))\]
\[\forall A, B, C, D, E, F \in \mathcal{O}, \forall \varphi \in \text{Sq}_{A,B,C,D}(f,g,p,q), \varphi' \in \text{Sq}_{C,D,E,F}(f',g',q,r),\] \[ \varphi' \circ_{\tau}^2\varphi \triangleq \circ^{C^1}(\varphi',\varphi)\]
\[\forall A, B, C, D, E, F \in \mathcal{O}, \forall \varphi \in \text{Sq}_{A,B,C,D}(f,g,p,q), \psi \in \text{Sq}_{B,E,D,F}(g,h,p',q'),\] \[ \psi \circ_{\lambda}^2\varphi \triangleq \ \text{comp}^m((\psi, \varphi))\]
\((``\Leftarrow")\)
In the other direction.
\[\text{ob}(C_0) \triangleq \mathcal{O}\]
\[\text{Mor}(C_0) \triangleq \{(A,B, f) \ :|: \ f \in \text{hom}_{\tau}(A,B)\}\]
\[\text{id}^{C_0}_A \triangleq (A, A, 1_A)\]
\[\circ^{C_0}((B,C,f'),(A,B,f)) \triangleq (A,C, f' \circ_{\tau}f)\]
\[\text{ob}(C_1) \triangleq \{(A,B, p) \ :|: \ p \in \text{hom}_{\lambda}(A,B)\}\]
\[\text{Mor}(C_1) \triangleq \{(A,B,p,C,D,q,f,g,\varphi) \ :|: \ \varphi \in \text{Sq}_{A,B,C,D}(f,g,p,q)\}\]
\[\text{id}^{C_1}_{(A,B,p)} \triangleq (A,B,p,A,B,p,1_A,1_B, \upsilon_p)\]
\[\circ^{C_1}(((A,B,p,C,D,q,f,g,\varphi),((C,D,q,E,F,r,f',g',\varphi')) \triangleq\] \[ (A,B,p,E,F,r,f'\circ_{\tau}f, g'\circ_{\tau}g, \varphi'\circ_{\tau}^2\varphi)\]
Define functors
\[s,t : C_1 \rightarrow C_0\]
by \(s^o((A,B,p)) \triangleq A\) and \(s^m((A,B,p,C,D,q,f,g,\varphi)) \triangleq (A,C,f)\).
Similarly, \(t^o((A,B,p)) \triangleq B\) and \(t^m((A,B,p,C,D,q,f,g,\varphi)) = (B,D,g)\).
Also define
\[\text{id} : C_0 \rightarrow C_1\]
by \(\text{id}^o(A) \triangleq (A,A,\text{id}_A)\) and \(\text{id}^m((A,B,f)) \triangleq (A,A,\text{id}_A,B,B,\text{id}_B,f,f,=).\)
Finally define
\[\text{comp} : C_1 \times_{C_0} C_1 \rightarrow C_1\]
by \(\text{comp}^o((B,C,q),(A,B,p)) \triangleq (A,C, q \circ_{\lambda}p)\) and \(\text{comp}^m((B,E,q, D, F, q', g,h,\psi),(A,B,p,C,D,p',f,g,\varphi)) \triangleq\)
\[(A,E, q \circ_{\lambda}p, C, F, q' \circ_{\lambda}p', f, h, \psi \circ_{\lambda}^2\varphi).\]
Whenever we talk of a double category we will mean the definition which starts with a class of objects and two hom-sets, as above.
Example 1 (The double category Rel) We will now describe \(\mathbb{R}\text{el}\) the double category of relations and functions. Firstly, \(\mathcal{O}\) is class of small sets then for sets \(A,B\) we define \(\text{hom}_{\tau}(A,B) \triangleq \text{hom}_{Set}(A,B)\) is set of all functions from \(A\) to \(B\) whereas \(\text{hom}_{\lambda}(A,B)\) is the set of relations \(A\) to \(B\) viewed as monomorphisms into \(A\times B\). The tight composition is simply composition of functions, while loose composition is defined as composition of relations. The squares are unique if they exist, and are witnessed to exist by the truth of the following logical formula
\[\forall (x,y) \in R \quad : \quad (f(x),g(y)) \in R'. \]
Where \(A, B, A', B'\) are sets, \(f : A \rightarrow A', g: B \rightarrow B'\) are functions and \(R: A \not\rightarrow B, R' : A' \not\rightarrow B'\) are relations. Tight composition of cells is the composition of functions while loose composition of cells is the composition of relations which are easily proven to exist by checking the truthfulness of the witness. The identity functions are the tight identities, \(1_A : A \rightarrow A\) is \(x \mapsto x\) and the loose identities is the diagonal relation, \(\text{id}_A = \Delta_A \subset A\times A\). The identity cells \(\upsilon_A\) are witnessed by the tautology \((x,y) \in R \Rightarrow (x,y) \in R\).
Example 2 (The double category IntBil) Next we will give a description of a double category inspired by multivalued logics. This will use the following (see Fitting 2020, Proposition 7.1)
Bilattices
Definition 7 (Bilattice) A Bilattice is a non-empty set \(\mathbf{B}\) with four distinct constants \(\mathbf{t}, \mathbf{f}, \bot, \top\) as well as four idempotent, associative and commutative binary operators \(\land, \lor, \otimes, \oplus\) which further satisfy, for every \(a, b \in \mathbf{B}\), absorbative conditions:
\(a\land(b\lor a) = a;\)
\(a\lor(b\land a) = a;\)
\(a\otimes(b\oplus a) = a;\)
\(a\oplus(b\otimes a) = a.\)
Finally, \(\mathbf{t}\) is the identity for \(\land\) (respectively, \(\mathbf{f}\) for \(\lor\), \(\top\) for \(\otimes\), \(\bot\) for \(\oplus\)).
Definition 8 A set function \(\varphi : (\mathbf{B},\land, \lor, \otimes, \oplus, \mathbf{t}, \mathbf{f}, \top, \bot) \rightarrow (\mathbf{B}^{\gimel}, \land^{\gimel}, \lor^{\gimel}, \otimes^{\gimel}, \oplus^{\gimel}, \mathbf{t}^{\gimel}, \mathbf{f}^{\gimel}, \top^{\gimel}, \bot^{\gimel})\) is called a bilattice morphism when it preserves each constant:
- \(\varphi(\mathbf{t}) = \mathbf{t}^{\gimel};\) \(\varphi(\mathbf{f}) = \mathbf{f}^{\gimel};\) \(\varphi(\top) = \top^{\gimel};\) \(\varphi(\bot) = \bot^{\gimel};\)
and each operator, for every \(a, b \in \mathbf{B}\):
\(\varphi(a \land b) = \varphi(a) \land^{\gimel} \varphi(b)\);
\(\varphi(a \lor b) = \varphi(a) \lor^{\gimel} \varphi(b)\);
\(\varphi(a \otimes b) = \varphi(a) \otimes^{\gimel} \varphi(b)\);
\(\varphi(a \oplus b) = \varphi(a) \oplus^{\gimel} \varphi(b)\).
Definition 9 (Interlaced Bilattice) A Bilattice \((\mathbf{B}, \land, \lor, \otimes, \oplus, \mathbf{t}, \mathbf{f}, \top, \bot)\) is called interlaced if the following two conditions are satisfied:
- for every \(a,b \in \mathbf{B}\) such that \(a \land b = a\), and for all \(c \in \mathbf{B}\):
\[ (a\otimes c) \land (b \otimes c) = a \otimes c, \quad \text{and} \quad (a\oplus c)\land (b \oplus c) = a \oplus c;\]
- for every \(d,e \in \mathbf{B}\) such that \(d \otimes e = d\), and for all \(f \in \mathbf{B}\):
\[ (d \land f)\otimes (e \land f) = d \land f, \quad \text{and} \quad (d\lor f)\otimes (e \lor f) = d \lor f.\]
For simplicity, we will from now on supress the extra data and simply write \(\mathbf{B}\) for the bilattice as a whole.
Proposition 1 (Bilattice morphisms preserve interlacing) Whenever \(\varphi: \mathbf{B} \rightarrow \mathbf{B}^{\gimel}\) is a bilattice morphism which is also bijective as a set function and further \(\mathbf{B}\) is an interlaced bilattice then \(\mathbf{B}^{\gimel}\) is also an interlaced bilattice.
Given two categories \(\mathcal{C}\) and \(\mathcal{D}\) which have, respectively, products and coproducts the twisted product produces a pair of categories with the same class of objects, simply the product of the classes of objects \(\text{ob}(\mathcal{C})\times \text{ob}(\mathcal{D})\). The tight category with non-decorated arrows is the product \(\mathcal{C} \times \mathcal{D}^{op}\) and the loose category with decorated arrows is the product \(\mathcal{C} \times \mathcal{D}\).
We will need to define products and coproducts for each category. The first of these, the product in the tight category \((A_1,A_2)\bowtie (B_1,B_2) \triangleq (A_1 \sqcap_{\mathcal{C}} B_1, A_2 \sqcup_{\mathcal{D}} B_2)\). A prior there is no reason why this should be a functor, even given functors \(\ltimes (B_1, B_2)\) and \((A_1,A_2) \rtimes : \mathcal{C} \times \mathcal{D} \rightarrow \mathcal{C}\times\mathcal{D}\) for fixed \((A_1,A_2), (B_1,B_2)\) that coincide still does mean that the coincidence becomes a functor. What is needed is the interchange law! We call the above situation a Binoidal category (see Levy et al. (2003) Appendix A, Power and Robinson (1997) Section 3, Román (2022) Section 2). We now ask not the interchange law to hold but for the centre of a Binoidal category, defined as the wide subcategory of morphisms which are central. For our specific case we say \(f:(A_1,A_2) \not\rightarrow (B_1, B_2)\) is central when for each \(g : (C_1,C_2) \not\rightarrow (D_1,D_2)\);
\[(f \bowtie \text{id}_{(C_1,C_2)}) ; (\text{id}_{(B_1,B_2)} \bowtie g) = (\text{id}_{(C_1,C_2)}\bowtie g) ; (f \bowtie \text{id}_{(D_1,D_2)})\] and \[(\text{id}_{(C_1,C_2)} \bowtie f) ; (g \bowtie \text{id}_{(B_1, B_2)}) = (g \bowtie \text{id}_{(A_1,A_2)}) ; (\text{id}_{(D_1,D_2)} \bowtie f).\]
Essentially, this unravels to be asking that each component of \(f = (f_1, f_2)\), \(f_1 : A_1 \rightarrow B_1\), \(f_2 : A_2 \rightarrow B_2\) is central. Which is guaranteed by the universal property of the product, and coproduct, respectively.
A Premonoidal category is a Binoidal category with coherence morphisms being central. A useful fact is that the centre of a premonoidal category is monoidal. Therefore, a premonoidal category equivalent to its own centre is immediately monoidal.
MSP 201
Topos Theory
Meeting 05/10/26
We started with the definition of subobject classifier given in Definition 1.1 of (Leinster10?)
Definition 10 (Subobject Classifier) Let \(\mathcal{E}\) be category with a terminal object, \(1\). A subobject classifier in \(\mathcal{E}\) is an object \(\Omega\) and an arrow \(t : 1 \rightarrow \Omega\) out of the terminal object satisfying the following condition: Given any monomorphism \(m : A \hookrightarrow X\) there exists a unique morphism \(\chi: X \rightarrow \Omega\) such that the following square is a pullback.
Checking our intuition first we began with showing that \(\Omega = \{0,1\}\) with \(t : 1 = \{\star\} \rightarrow \Omega\) mapping to \(1\) is indeed the subobject classifier. The repeated situation that occured again and again is that there are neccessary choices for \(\chi\) by the commutativity of square (this assumes we are working in a concrete category which is reasonable for our examples). Then the uniqueness occurs when considering the pullback condition.
We next consider the category \(\mathcal{S}\text{et}^{B\mathbb{N}}\) which can be instead thought of as the category of dynamical systems, this means nothing more than a set with a self map called the update function. These dynamical systems can viewed through little pictures, \(\mathcal{D}\text{yn}\mathcal{S}\text{ym}\) is equivalently \(\Omega(1)\) the category of unary algebras. The morphisms of this category are then graph homomorphism, equivalently unary algebra homomorphisms, furthermore the monomorphisms are simply injective unary algebra homorphisms. This is a clearly a very nice category to work with for intuition.
We now looked at trying to write down what the subobject classifier is for unary algebras. The first pass intuition was to consider the graph of natural numbers with \(0\) as a sink and arrows decrementing by 1. Other attempts included the graph of natural numbers with successor. This lead us to think about adding a place of absolute untruth as somewhere inaccessible from anywhere else. We then asked why we couldn’t simply have the discrete graph on 2 points. Finally thinking about a game between 2 players one trying to find the correct subobject classifier and the other trying to break with continued counterexamples produced the original first pass but we also realised that we needed to reintroduce the place of untruth from before. The final answer is summarised below.
Sieves are the oidification of right ideals for monoids. By viewing \(\Omega(1)\) as presheaves on the delooping of \(\mathbb{N}\) we can just consider right ideals of the natural numbers under addition. The formula for the subobject classifier for presheaf categories gives us exactly the same as above with 0 standing for \(\mathbb{N}\), 1 for \(\mathbb{N}\setminus\{0\}\), 2 for \(\mathbb{N} \setminus \{0, 1\}\) and so on… until \(\bot\) is exactly empty.