The distinction between objects and morphisms lies at the heart of elementary category theory. In order to create a coherent logical narrative, we need to move beyond this distinction.
Background
Mathematics cannot be completely separated from philosophy. There is always some basic philosophical framework that addresses questions of logic, ontology, mathematics, and their relationship to one another. This philosophical framework consists of a series of conditions placed on mathematical structures.
A first condition I have is that every mathematical object should have some kind of logically comprehensible structure. I have always had the desire that every mathematical object, or even every computational entity, should have comprehensible logical innards. Set theory solves this problem by modeling mathematical entities as sets.
The first entity that you can imagine that has a well defined logical structure is a set. The parts of a set can be modeled as subsets, which defines a logically reasonable structure on sets. Set theory certainly provides an initial solution to our problem of giving every mathematical object intelligible innards.
The problem is the intelligible innards you get are all wrong. It at least gets an internal structure for a mathematical object, but for anything involving functions the results we not all what we want. Topos theory is needed for us to get to the right logical structure of mathematical objects like functions and to create a coherenent logical narrative of mathematical structures.
In order to create a well defined logical structure a minimum necessary condition is to define a partial order, which relates a structure to its parts. This logical notion can be extended by using categories, which generalise partial orders. We need to make morphisms part of some logical structure so tha they have comprehensible innards. This problem is solved by making morphisms into objects.
Morphisms have morphisms too
Set theory can be made categorical by defining functions to be the morphisms between sets. The resulting topos $Sets$ is perhaps the quintessential example of a category.
- Objects: sets
- Morphisms: functions
The problem is that functions $f : A \to B$ don't have morphisms of their own. We can solve this problem by introducing morphisms of functions from $f: A \to B$ to $g : C \to D$ as ordered pairs $(i : A \to C, o : B \to D)$ that satisfy a commutative diagram:
What do we gain by this construction? This makes it so that we can define precisely the intelligible innards of functions we want. These are exposed as the subobject and congruence lattices of objects of the topos $Sets^{\to}$. This gets around the apparent lack of a logic describing functions.
Every function $f : A \to B$ can now be understood in terms of its parts. These parts are either subfunctions determined by subalgebras or quotient functions determined by congruences. We can finally reason logically about functions and reduce to them to their constituent parts. We did this by introducing morphisms of functions, so we wonder if we can reason about them logically too.
If we look back at that commutative diagram, we can think of a number of different ways to reduce its constituent sets and functions. A notable fact about functions is that given $f : A \to B$ and $S \subseteq A$ there is always a subobject $f|_S : S \to B$ in the topos functions determined by restriction. A natural generalisation is that we can take any subobject $(S,T)$ of the source function $f: A \to B$ of a morphism of functions and restrict it to that subobject. This is in fact equivalent to a composite diagram.
So there a number of ways to get subobjects of morphisms of functions, but the same process can even be extended. We can even get subobjects of morphisms of functions by getting subobjects of the target function as long as those the elements removed are not in the image of the first function $i$ or the second function $o$. So there are a number of ways of getting subobjects of morphisms of functions by restricting any of its four sets.
At this point we can introduce the topos of diamonds. Morphisms of functions form a diamond shaped commutative diagram, so that they are essentially copresheaves over the diamond category. Subobjects and quotients of morphisms of functions are then defined in terms of this topos. The previous subobject of a morphism of functions is now defined in terms of a cube diagram:
The topos of diamonds consists of morphisms of functions as its objects and cube natural transformations like these as its morphisms. This means not only do functions have their own morphisms, but their morphisms of functions do as well. We get the following sequence of morphisms:
Set $\to$ Function $\to$ Diamond $\to$ Cube
This can be extended infinitely as well, so that next we can get morphisms of cubes. Then cubes have their own subobjects and quotients and so on. We finally get an infinitely extensible framework aside in which each entity has its own intelligible innards. This loses none of the logical cohesiveness that we had before.
Morphisms of copresheaves
Let $Sets^C$ be a topos of copresheaves over $C$. Then we consider morphisms in the topos $Sets^C$ in terms of objects of the topos $Sets^{C \times T_2}$. This means that morphisms of copresheaves are themselves copresheaves.
Definition. Let $P \in Ob(Sets^{C \times T_2})$ be a copresheaf. Then 0 and 1 form trivial subcategories of $T_2$ so by extension so do $(C,(0,0))$ and $(C,(1,1))$ of $C \times T_2$. These subcategories induce inclusion functors, and by composition this allows us to produce copresheaves $P_0$ and $P_1$ of $P$ in $Sets^{C}$. Then we form a morphism $P_0 \to P_1$ in $Sets^C$ with component arrows $(1_A, (0,1))$ in $Sets^{C \times T_2}$ for each object $A \in Ob(C)$.
Theorem. the preceding definition is a valid morphisms of copresheaves
Proof. let $m : A \to B$ be an arrow in $C$. Then $P_0(m) = (m,(0,0))$, $P_1(m) = (m,(1,1))$, $\tau_A = (1_A, (0,1)$, and $\tau_B = (1_B, (0,1))$. It remains to show that $P_1(m) \circ \tau_B$ is equal to $\tau_A \circ P_0(m)$. By substitution we have $P_1(m) \circ \tau_B = (m,(1,1)) \circ (1_B, (0,1))$ but this equals $(m,(0,1))$. Similarily, by substitution we have that $\tau_A \circ P_0(m)$ is equal to $(1_A,(0,1)) \circ (m,(0,0))$. This equals $(m,(0,1))$. So the two compositions coincide. $\square$
Definition. let $F$ and $G$ be copresheaves in $Sets^C$ with a morphism $\tau : F \to G$. Then we can define a copresheaf $P$ in $Sets^{C \times T_2}$. Let $O \in Ob(C \times T_2)$ then $P(o,n)$ is equal to $F_o$ if $n=0$ and $G_o$ if $n=1$. On the other hand let $M : X \to Y \in Arrows(C \times T_2)$. Then there are three cases for $P(M)$ if it is equal to $(m,(0,0)$ then we get $F_m$, if it is equal to $(m,(1,1)$ it is equal to $G_m$, finally if it is $(m,(0,1))$ it is equal to $\tau_Y \circ F(m)$ or $G(m) \circ \tau_X$.
Theorem. the preceding definition produces valid copresheaves
Proof. let $(C_1 : Y \to Z, t_1)$ and $(C_2 : X \to Y, t_2)$ be morphisms in $C \times T_2$. Then there are four patterns of composition.
(1) if $t_1$ and $t_2$ are equal to $(0,0)$ then we get that
\[ P((C_1 : Y \to Z, (0,0)) \circ (C_2 : X \to Y, (0,0))) \]
\[ = P(C_1 \circ C_2, (0,0)) = F(C_1) \circ F(C_2) \]
At the same time, $P(C_1 : Y \to Z, (0,0))$ is equal to $F(C_1)$ and $P(C_2 : X \to Y, (0,0))$ is equal to $F(C_2)$ so the two compositions coincide.
(2) similarily if $t_1 = t_2 = (0,0)$ then we get the following
\[ P((C_1 : Y \to Z, (1,1)) \circ (C_2 : X \to Y, (1,1))) \]
\[ = P(C_1 \circ C_2, (1,1)) = G(C_1) \circ G(C_2) \]
If we plug in $P(C_1 : Y \to Z, (1,1))$ is equal to $G(C_1)$ and $P(C_2 : X \to Y,(1,1))$ is equal to $G(C_2)$ so the two compositions coincide.
(3) in the third case $t_1 = (0,1)$ and $t_2 = (0,0)$
\[ P((C_1 : Y \to Z, (0,1)) \circ (C_2 : X \to Y, (1,1))) \]
\[ = P(C_1 \circ C_2, (0,1)) = \tau_Y \circ F(C_1) \circ F(C_2) \]
\[ = (\tau_Y \circ F(C_1)) \circ F(C_2) = P(C_1,(0,1)) \circ P(C_2,(1,1)) \]
This confirms that these two compositions coincide.
(4) in the third case $t_1 = (1,1)$ and $t_2 = (0,1)$
\[ P((C_1 : Y \to Z, (1,1)) \circ (C_2 : X \to Y, (0,1))) \]
\[ = P(C_1 \circ C_2, (0,1)) = G(C_1) \circ G(C_2) \circ \tau_Y \]
\[ = G(C_1) \circ (G(C_2) \circ \tau_Y) = P(C_1,(1,1)) \circ P(C_2,(0,1)) \]
This confirms that $P$ is a valid functor. $\square$
Infinitely categorical:
In order to get to our philosophical goal of every mathematical entity having a comprehensible logical structure, we have to have every mathematical entity be an object of some category. We saw this when we introduced morphisms of functions, and then further morphisms on top of those as well.
At no point should we reach an endpoint where we have a morphism, which doesn't have any further morphisms of its own. This gets to the philosophy of infinity category theory, in which each morphism has its own morphisms extended on to infinity. This is a process that we started with sets and functions.
Presheaf foundations:
The importance of this construction is that it means that presheaf theory is stable under taking objects and morphisms. This means that presheaf theory can truly be used as a foundation of mathematics. The importance of this approach is that it gives the best logical structure to mathematics and its constructs.
The Locus project puts this philosophy into practice. It represents structures as much as possible as presheaves, and it makes their logical structure available to the user. This is to be combined with an ontology of classes of copresheaves and a graphical user interface program for interacting with copresheaves. This is the start of the new approach to topos theory.
So that previous image has a bunch of lines clipped inside of its circle. So one thing we can do is instead placing those lines outside the circle to get something like this.
The previous example is a bit elementary. We can do a lot more if we get some interesting paints involved like the radial gradient paint.
As we will see there is much more that can be done with the Java 2D graphics API. It is readily available in both Java and Clojure.
