Embarassingly parallel decompositions of functions

A basic primitive of functional programming, the map function, is embarrassingly parallel. This means that map can be broken up into independent computations requiring no communication or synchronization between them except for a join operation at the end. It would be nice if we could describe embarrassing parallelism in the most general sense using category-theoretic universal properties.

To do this we will use the topos $Sets^{\to}$. It will be shown that products in this category describe embarrassingly parallel computations. If $X^n$ is the set of $n$-tuples of elements of $X$, then the map function with argument $f$ is equivalent to the product function $f^n$ of $f$ with itself $n$ times. We will describe how arbitrary functions in $Sets^{\to}$ can be given product decompositions, even when they do not use representations by sequences so that they can be treated as embarrassingly parallel functions.

Background on the algebraic theory of information:
The algebraic theory of information, introduced by Hartmanis and Stearns requires that we model information using partitions. In modern categorical treatments, partitions are equivalence classes of epimorphisms in the topos $Sets$. As every topos, including $Sets$, has epi-mono factorizations, every function in $Sets$ has an epi-component which is its partition or kernel.

Definition. let $f$ be a function then $f$ defines a partition called $ker(f)$ which describes equality with respect to $f$: \[ (a,b) \in ker(f) \Leftrightarrow f(a) = f(b) \] Example 1. let $\Omega : \{0,\frac{1}{2},1\} \to \{0,1\}$ be the object of truth values in $Sets^{\to}$ then its kernel is the equivalence relation defined by the partition $\{\{0\},\{\frac{1}{2},1\}\}$

Example 2. let $abs : \mathbb{R} \to \mathbb{R}$ be the absolute value function. Then $(-1,1) \in ker(abs)$ because $-1$ and $1$ have the same absolute value.

Background on products in Sets:
Definition. let $S_1,S_2,...S_n$ be a family of sets in the topos $Sets$. Then a universal product cone is a family of epimorphisms $f_i$ from an object $X$ to each $S_i$. By the kernel construction it follows that each $f_i$ has a corresponding partition $ker(f_i)$. These partitions have the following property: \[ \forall F \in \prod_{i \in I} P_i: |\bigcap_{i \in I} F_i| = 1 \] Which equivalently states that each selection of equivalence classes for each partition has a single common intersection. To demonstrate the use of this formalism we have provided a set of examples:

Example 1. {{0,1},{2,3}} and {{0,2},{1,3}} form a product decomposition because all pairs of equivalence classes between them have singular intersection:

	0,2	1,3
0,1	0	1
2,3	2	3

Example 2. {{0,1,2},{3,4,5},{6,7,8}} and {{0,3,6},{1,4,7},{2,5,8}} form a product decomposition because all pairs of equivalence classes between them have singular intersection:

	0,3,6	1,4,7	2,5,8
0,1,2	0	1	2
3,4,5	3	4	5
6,7,8	6	7	8

Example 3. the following three equivalence classes form a product decomposition because all triples of equivalence classes chosen between the three of them have singular intersection: \[ \{\{0,1,2,3\}, \{4,5,6,7\} \} \] \[ \{\{0,2,4,6\}, \{1,3,5,7\} \} \] \[ \{\{0,1,4,5\}, \{2,3,6,7\} \} \] This can be confirmed by examining all the triples of equivalence classes of these three partitions manually to determine that they have singular intersection: \[ \{0,1,2,3\} \cap \{0,2,4,6\} \cap \{0,1,4,5\} = \{0\} \] \[ \{0,1,2,3\} \cap \{0,2,4,6\} \cap \{2,3,6,7\} = \{2\} \] \[ \{0,1,2,3\} \cap \{1,3,5,7\} \cap \{0,1,4,5\} = \{1\} \] \[ \{0,1,2,3\} \cap \{1,3,5,7\} \cap \{2,3,6,7\} = \{3\} \] \[ \{4,5,6,7\} \cap \{0,2,4,6\} \cap \{0,1,4,5\} = \{4\} \] \[ \{4,5,6,7\} \cap \{0,2,4,6\} \cap \{2,3,6,7\} = \{6\} \] \[ \{4,5,6,7\} \cap \{1,3,5,7\} \cap \{0,1,4,5\} = \{5\} \] \[ \{4,5,6,7\} \cap \{1,3,5,7\} \cap \{2,3,6,7\} = \{7\} \] Each of these eight triples are families of sets in the product $\prod_{i \in I} P_i$ that have singular intersection.

Product functions:
Definition. let $f_i: A_i \to B_i $ be a family of functions then their product in $Sets^{\to}$ is the function: \[ \prod_{i \in I} f_i : \prod_{i \in I} A_i \to \prod_{i \in I} B_i \] That is defined by applying the function $f_i$ to the value at index $i$ of a sequence in $\prod_{i \in I} A_i$: \[ \prod_{i \in I} f_i(a_1,...a_n) = (f_1(a_1),...,f_n(a_n)) \] Example 1. let $f: X \to Y$ be a function then $f^n: X^n \to Y^n$ is the function that applies the higher-order map function to sequences of size $n$ using the function $f$.

Example 2. let $inc: \mathbb{R} \to \mathbb{R}$ be the function $inc(x) = x+1$ and let $double : \mathbb{R} \to \mathbb{R}$ be the function $double(x) = 2*x$. Then the function $inc \times double : \mathbb{R}^2 \to \mathbb{R}^2$ has $f(x,y) = (x+1, 2*y)$.

The critical characteristic of product functions is that they are embarrassingly parallel. Given a product function $f \times g$, the results of the functions $f$ and $g$ can be computed entirely separately from one another. Then all we need to do is combine the results of these separately computed values at the end to get a final result.

Category theory teaches us that we can treat products using universal properties instead of by reference to their common representations. The product of sets is not necessarily a set of ordered pairs but rather a universal limiting cone, and that is one of its representations. To move beyond issues of representation, we will also have to consider universal cones in $Sets^{\to}$.

Embarassingly parallel decompositions:
Proposition. let $f: A \to B$ be a function in $Sets^{\to}$. Then a decomposition of $f$ into separate information flows is a family $(P_1,Q_1), (P_2,Q_2), ... (P_n,Q_n)$ of information flows such that the source partitions $P_1, P_2, ... P_n$ form a product decomposition of $A$ and the target partitions $Q_1, Q_2, ... Q_n$ form a product decomposition of $B$.

Example 1. let $f(a,b) = (a+1,b+1)$ then ((0,0), (1,1)) form a family of flow relations where (0,1) and (0,1) are both product decompositions. These information flows produce a universal limiting cone in $Sets^{\to}$: Example 2. let $f(a,b) = (b,a)$ be the transposition function then $((0,1),(1,0))$ forms a family of flow relation where (0,1) and (1,0) are both product decompositions. These information flows produce a universal limiting cone in $Sets^{\to}$: We see now that to reconstruct a product function from a family of independent information flows, you only need to take the product of all its quotients. This demonstrates how the theory of information flows in the topos of functions $Sets^{\to}$ can be used to create embarassingly parallel decompositions.

References:
[1] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines.

[2] Bernier, J. (2023). Toposic structure theory of computations.

[3] Goldblatt, R. (2014). Topoi the categorial analysis of logic. Elsevier Science.

A comparative study of structure theories

The most groundbreaking work in the computer industry was essentially done in the late 1950s to the 1960s, because there wasn't much ground to break yet. The Algebraic Structure Theory of Sequential Machines (1966) owes its origin to that era. Every single computer science treatise now owes something to that time, and most ones have broad similarity to something back then. But the similarities often end there, as examinations of any modern theory always exposes key differences.

That is also the case with the topos theory of computations. While the basic intuitive framework is the same as Hartmanis and Stearns, all technical aspects of the theory are different. In 2023, a preliminary research paper Toposic Structure Theory of Computations (2023) was released with this new and updated theory. If this is well recieved, a full textbook on the the topos of computation, containing the advanced theory, will be produced.

With these two structure theories now widely available for consideration, it is high time that a comparative study was conducted to highlight their similarities and differences. In this study, we will describe why it is so necessary that a new and updated theory should be produced. The value brought about by the application of new techniques in categorical logic and topos theory will be described and the limitations of the classical theory will be considered.

Background and motivation:
The theory of Hartmanis and Stearns was designed with engineering applications in mind. To quote their text, "The engineering motivations demands new mathematical techniques to be invented with no counterpart in the development of algebra. Thus, this theory has a characteristic flavour and mathematical identity of its own." As a consequence, they developed the idea of information flows with its engineering applications in mind.

On the other hand, the Toposic Structure Theory of Computations (2023) is a purely mathematical treatise. It was created with the idea of exploring an aspect of topos theory in mind. That the topos it studies happens to be the topos of computations is a convenient coincidence, that makes this study worthy of publication and wide spread dissemination. This text should be of interest even to pure mathematicians working in topos theory.

Scope:
The Algebraic Structure Theory of Sequential Machines (1966) studies information flows with respect to sequential machines. These are treated as transition functions $\delta: S \times I \to S$ on a set of states $S$ and a set of inputs $I$. In effect, however, they are families of functions $\delta : S \to S$ for each $i \in I$. Then a partition pair of $\delta$ for $(P,Q)$ says that for each $i \in I$ : $s =_P t \Rightarrow \delta(i,s) =_Q \delta(i,t)$.

They never consider to examine what a partition pair $(P,Q)$ be defined an a single function $f: A \to B$ would mean. Already in section 0.1 of their text, on "sets and functions" you can see that they are hopelessly lost in the old ways of set theory. The great mental liberation and significant technical advantages of modern topos theory were not considered.

That is why they define information flows always for families of functions $\delta_i$ rather then considering them individually. If they'd taken the later perspective, their theory would have had better foundations. This approach produces a theory with very limited scope and applicability. It is no wonder then why this theory was hardly ever used and history went the way it did.

By contrast, the Toposic Structure Theory of Computations (2023) is applicable to any kind of functional computation. This produces a theory with far greater and wider applicability than ever before, and it exposes all functions to the logic of information flows. This is really a paradigm shift and a transition from foundations in the topos $Sets$ to the topos $Sets^{\to}$.

Mathematical context:
In the Toposic Structure Theory of Computations (2023) we study the topos $Sets^{\to}$ and its morphisms. These are ordered pairs of functions $(i,o)$ between functions $f$ and $g$ that form commutative diagrams like so: Then $(i,o)$ has an epi-mono factorisation like so: There are your partition pairs $(P,Q)$ emerging right out of morphisms in the Sierpinski topos. They exist between individual functions. A morphism in the topos $Sets^{\to}$ is the embedding of the information flow of some function in another. The algebraic approach to information, it turns out, is nothing more then the logic of the topos $Sets^{\to}$.

By taking this categorical perspective we are able to create a far richer theory than the classical one of Hartmanis and Stearns. The effects of morphisms in $Sets^{\to}$ on information flows is considered categorically, leading to a number of interesting results. Functorial semantics for information flows are developed. None of this would be possible without the use of new developments in category theory.

Conclusions:
The prior work of Hartmanis and Stearns on the algebraic theory of information is inspiring. Any further work in the algebraic theory of information should mention their fundamental work and give proper credit where it is due. Nonetheless, their approach is frought with a number of limitations: limited scope, a lack of category theory, underdeveloped mathematical foundations. This is solved by creating a new theory.

References:
[1] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.

Visualising information flows of finite functions

One way that I can demonstrate that information flows is through visualisation. That information flows form a lattice can be seen intuitively by realising that if the information in $P_1$ determines the information in $Q_1$ and the information in $P_2$ determines the information in $Q_2$ then the combined information $P_1P_2$ determines the information in $Q_1Q_2$. That they form a lattice also means they can be displayed as Hasse diagrams, so you can see what they look like.

All visualisations will be done with Clojure and Graphviz. In order to create set theoretic functions, we need the data of an input set, an output set, and a Clojure function or map. This ensures that we can handle functions that are not surjective. But in the easier case where they are surjective, we can just get a function using the to-function method. The elements of the information flow lattices are partition pairs, which are vectors of disjoint families of sets.

Small functions:

(SetFunction. #{0} #{0} {0 0})

(SetFunction. #{0 1} #{0} {0 0, 1 0})

(SetFunction. #{0 1} #{0 1} {0 0, 1 1})

(SetFunction. #{0 1} #{0 1} {0 0, 1 0})

(SetFunction. #{0 1 2} #{0} {0 0, 1 0, 2 0})

(SetFunction. #{0 1} #{0 1 2} {0 0, 1 1})

(SetFunction. #{0 1 2} #{0 2} {0 0, 1 0, 2 2})

(SetFunction. #{0 1 2} #{0 1 2} {0 0, 1 1, 2 2})

Intermediate sized functions:

(to-function {0 0, 1 0, 2 0, 3 0})

(to-function {0 0, 1 0, 2 2, 3 2})

(to-function {0 0, 1 0, 2 0, 3 3})

(to-function {0 0, 1 1, 2 2, 3 2})

(to-function {0 0, 1 1, 2 2, 3 3})

(to-function {0 0, 1 0, 2 0, 3 0, 4 0})

(to-function {0 0, 1 0, 2 2, 3 2, 4 2})

(to-function {0 0, 1 0, 2 0, 3 0, 4 4})

(to-function {0 0, 1 0, 2 0, 3 3, 4 4})

(to-function {0 0, 1 1, 2 1, 3 3, 4 3})

(to-function {0 0, 1 1, 2 2, 3 3, 4 3})

(to-function {0 0, 1 1, 2 2, 3 3, 4 4})

Large or infinite functions:
By generality, functions larger then these have information flow lattices even if we cannot visualize them. The algebraic theory of information ensures that we can exist. Using mathematical techniques we can describe their properties even in the infinite case.

References:
[1] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.

[2] Lausmaa, T. (2005). Extropy-based quantitative evaluation of finite functions. Proceedings of the Estonian Academy of Sciences. Physics. Mathematics, 54(2), 67. https://doi.org/10.3176/phys.math.2005.2.01

Paying homage to the work of Hartmanis and Stearns

A commenter alerted me to the fundamental work of Hartmanis and Stearns: Algebraic Structure Theory of Sequential Machines (1966). This came closest to capturing the fundamental ideas that I was getting at in my study of information flows. To put my work in context, I want to do something to pay homage to this prior work.

When I first thought about what to title my paper, I couldn't think of anything particularly good that would stick. So I took the good old fashioned shotgun approach and made a big title with a bit of everything: "The Topos Theory of Computing: Introduction to the Mathematics of Dataflow." Yet its clear that calling this a theory of computing doesn't get to the point, because the whole point of this thesis is an examination of structures.

By changing the title of my work to Toposic Structure Theory of Computations (2023) I get an intrinsically better title while also more effectively paying homage to the excellent prior work of Hartmanis and Stearns. This hopefully reduces any controversy around my work and puts it into an appropriate historical context. We now have two different types of structure theory in computer science:

• The algebraic structure theory
• The toposic structure theory

The Algebraic Structure Theory of Sequential Machines (1966) is one of those marvelous gems of science and technology that due to historical accident seems to have fallen to the way side. It is something that despite its age still has something to teach us, just like the Lisp machines. There is always something to be learned from studying the best technologies of the past.

But I am not here to revive old technologies. In my work, I developed novel new foundations for the mathematics of information flows using topos theory. It is demonstrated that the information flows of Hartmanis and Stearns are nothing more then quotients in $Sets^{\to}$. By establishing functors from a wide variety of different categories to $Sets^{\to}$ information flows are applied to a wider variety of contexts then ever before.

It is shown that morphisms in $Sets^{\to}$ preserve and reflect partition pairs. The result is a monotone Galois connection between information flow lattices of functions associated to every morphism in $Sets^{\to}$. This opens up a wide variety of different computations that would not be possible without the topos theoretic framework. All of this makes this subject an exciting and fertile ground for further exploration.

References:
Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.

A new way of programming with information flows

Informal discussion:
The physical world is highly parallel, with many things happening side by side. A realistic model of computation is dataflow, which can be conceptualized as a kind of motion. Much like how particles move around in physical systems, bits of information move around in computers. This motivates our development of a theory of information flows.

But what exactly are these bits of information? Consider even and odd; then both are bit-valued functions that produce ones and zeros. But even and odd produce the same bits of information. They represent the information in two different ways. If $n$ is even then we know it is not odd, and if its not even then we know it is odd. The same applies the other way around.

To represent the same bit of information as evenness or oddness, we can use a partition. Both the even and odd functions are representations of the abstract notion of parity, which can be defined as a partition with two elements. An abstract bit of information is then a partition of a set into two different classes. It does not matter rather you get the parity from even, odd, 2 * mod(n,2), or any other representation. An abstract bit of information may be realized in many different forms.

A piece of information, in general, is just a collection of bits of information. We can call these partitions, but the important point is that they refer to a place within the information of a larger structure. A piece of information is larger than another one if it has more bits than it. Partitions abstract functions so that every function can now be treated as a representation of a piece of information.

We now know how to think abstractly about places within an information system, but we still need to understand how information moves around. Let $f: A \to B$ be a function; then we can describe a flow relation on $f$ by a pair (P,Q) which proclaims that the function moves the information in the place $P$ to the place $Q$. We now have a fundamental notion of information flows.

As an example, return back to our notion of parity. If we take a function like $x+1$ then we see that $x+1$ maps the parity information in its input to the parity information in its output. So (parity, parity) is a datflow relation on $x+1$. If we take an even number and add one to it, then we get an odd number and if we take an odd number and add one to it we get an even number. So $x+1$ flips parity bits around.

On the other hand, $x^2$ leaves the parity bit as it is: the square of an even number is even, and the square of an odd number is odd. Two other examples are $2x$, which always produces a number of even parity, and $2x+1$, which always produces one that is odd. Other functions like $\Omega$ might not map parities back to parities at all. These functions might take different numbers of the same parity and map them to numbers of different parities.

It would be nice if we could take a place in an input structure, like the parity of a number, and then find out exactly what place in the output it flows into. By doing this, we will depart from the traditional view of set theory which is that functions values in sets and instead make them take values in partitions.

In fact, we can do this if we take the notion of a partition image $f(P)$. This produces the set of information we know from $f$ when it is given the information in $P$. So the partition image directly codifies how a function moves information from places to places, and it lets you compute how a function moves bits from one location back to another. The dual concept is the partition inverse image $f^{-1}(Q)$, which is the collection of all bits of information that map into $Q$.

Partition images are the basis of our new way of programming with dataflow relations. A whole new parallel universe of functions that take operate on partitions is created alongside those that take values in sets. This is a new paradigm of computing in information systems which we call functional dataflow.

We provide a system of support for smart functions: special data types of functions that know things about their own data flow characteristics. These are combined with special partition data types, so that smart functions can have computable partition images. They can take a place in a system and return the place it maps to. This makes information flows accessible to the user.

As a basic example, consider a transposition permutation on pairs. Then this function swaps the order in an ordered pair $f(x,y) = (y,x)$. We might make this into a smart function that records its own flow information so that it records that the information in the first index is moved to the second index, and the information in the second is moved to the first. This flow information might be made computable using partition images, so that if you $f$ what it maps the first index to it will return the second index.

If bits of information are the simplest units of storage, then this suggests that bit-flow relations $(P,Q)$ between bits of information $P$ and $Q$ are the simplest forms of dataflow. We already saw an example of a bit flow relation with the (parity, parity) relations in arithmetic functions. These bit-flow relations are the atomic building blocks for all other dataflow relations.

Information flows can now be seen to form an ordering by scale. There can be large events with millions of bits moving around to ones with only one or two. By the same token, an event in a physical system might have anything from the motion of an astronomical body on the higher end to the motions of subatomic particles on the smallest scales. In both cases, we have an intuitive notion of scale. We now have a way of capturing information flows from the smallest scales to the largest.

For technical experts:
For aficionados of functors, categories, adjunctions, toposes, lattices, lenses, theorems and proofs: the topos structure theory of computing

Toposic structure theory of computations FAQ

As I present this new thesis on the role of topos theory in computing to the world, I have anticipated a number of possible questions and answers ahead of time. I will do my best to answer any questions you may have.

What prior work is closest to yours?
With the help of a commentor on hacker news, I have determined that the Algebraic Structure Theory of Sequential Machines (1966) comes closest my work. Most impressively, they came close to developing the idea of a dataflow relation without using Sierpinski topos theory. Instead of an ordinary algebraic structure theory, I provide an updated theory based instead upon topoi.

What other prior works do you build upon the most?
The first and foremost is probably Robert Goldblatt's Topoi: The Categorial Analysis of Logic. It is with this text that I first discovered the Sierpinski topos which opened up the way for my own further studies in the subject. A second reference text is Sketches of an Elephant – A Topos Theory Compendium. Aside from these a variety of lattice theory textbooks and papers provided extra tidbits of information.

What is the practical basis of applied topos theory?
I believe the answer to this is the principle of locality. The physical universe of which we are all a part is organized around this principle which states that an object is influenced directly only by its immediate surroundings. This creates an organizing principle of relevance to all fields of engineering. In classical physics this motivates the modeling of physical systems based upon their local behaviour. In computing, this motivates our theories of local computation and dataflow.

What use is a topos theory of computing?
The topos theory of computing can be used to model information loss and information flow. The first is relevant because the second law of thermodynamics states that the entropy of a logical system cannot decrease - which implies that information loss leads to heat dissipitation. The second is relevant because the principal of locality necessitates that computer systems should be modeled in terms of information flows and local effects.

What is this topos theory of computing?
I would like to explain it by analogy to physics. In physics we study the movement of particles from place to place. In this theory of computing, we instead study the movement of packets of bits from place to place. In order to describe these information flows I have presented a new formalism based upon Sierpinski topos theory.

Toposic structure theory of computations

Abstract:
The theory of data-flow analysis of computer programs has been extensively studied. The increasing need for dataflow analysis in the automatic parallelization of computer programs motivates the development of mathematical foundations for this field. We present a new approach to program dataflow analysis that incorporates partition lattices and the Sierpinski topos.

Link:
The topos theory of computing: introduction to the mathematics of dataflow

Locus 1.5

Locus 1.5 has been pushed to github. I would say the impetus for the recent series of changes was so that I could implement various categorical adjunctions that generalize images/inverse images. Towards that end, I have a multimethod for images and preimages which dispatches its arguments based upon the type of both of its values. So we have that images can be formed from various function-like objects applied to various mathematical objects.

• Set images are applicable to partial functions and multi-valued functions as well as ordinary functions. The image of a set under a multivalued function or set relation can be formed by the image multimethod.
• In most textbooks on category theory there is a mention of the topos $Quiv$ of binary quivers, which consists of two parallel functions from the edge set to the vertex set. I have generalized this to ternary quivers, and indeed all the way to nary quivers. The nary quivers implementation is new in this version.
• Given any nary quiver there are set images and inverse images: the set image of a set of edges in a nary quiver is the union of the sets of vertices in each edge, or in other words the union of all set images of the set under each component function. Inverses images are uniquely defined so that they form an adjunction.
• I implemented two new concepts for completions sake: partial quivers and hyperquivers. A hyperquiver is a functor from the parallel arrows category $T_{2,n}$ but to $Rel$ instead of $Sets$. Partial quivers are defined the same way but using te subcategory of partial functions. Set images under hyperquivers are formed by the union of all set images produced by all hte multivalued functions of the hyperquiver.
• Set images are defined for MSets and so instances of the MSet class implement the image multimethod now. The image of a set under an MSet is the set of all outputs of all actionts on the MSet applied to all elements of the set. Inverse images are defined dually so they form an adjunction.
• Images and inverse images are defined for set partitions. So that given a function you can apply it to a SetPartition rather then a set and you will get the appropriate set partition as an output using the image multimethod. This implements the adjunction between partition images and inverse images.
• Likewise, given any preorder you can apply it to a function instead of a set to get the preorder image or inverse image.
• The adjointness definition of continuous maps is defined by topological images/inverse images. So given a member of the TopologicalSpace class, it is interpreted properly by the image method to get an output topological space which is the maximal topological space which makes that map continuous. Topological inverse images are also defined so this forms an adjunction. So images/inverse images work in the most contexts possible now.
• A new class of copresheaves: Galois copresheaves is implemented now. These are just Galois connections without any reference to any underlying ordering.
• A new order theory framework integrating adjunctions is provided. New classes for residuated maps, coresiduated maps, and Galois connections are defined. The framework for supporting adjunctions has been greatly improved, motivated by this work on images and inverse images.
• Finally, new support for ordered algebraic structures is provided by new classes. These will be the first step towards algebraic structures like quantales which can always be formed from any algebraic structure using images and inverse images.

The implementation of the images/preimages framework is a good and necessary first step. A great many categories are defined by image/inverse image adjunctions, but the next steps will see us further improve the support for structure presheaves. Structure presheaves are our main focus.

Locus 1.4

The newest Locus version has been released to github. I have made several changes to make this program better organized.

• I have added special support for dealing with copresheaves over product and coproduct categories. A copresheaf over a product category $F: C \times D \to Sets$ is a simultaneously a bifunctor and a copresheaf. Support for the hom functor $Hom : C^{op} \times C \to Sets$ is provided with this new framework so for example we can deal with the Yoneda embedding. Support for copresheaves over coproducts is provided by index sums.
• Several improvements have been made in the compositional quivers framework introduced and developed in Locus 1.3. As mentioned previously, the presheaf topos theory of categories now has two components: the theory of Yoneda embeddings and the theory of compositional quivers.
• Corresponding to the support for hom bicopresheaves, we also have new classes to deal with the functor of points and its dual, the basis of representable presheaves and copresheaves used in the Yoneda embedding.
• Recall the definition of the arrow category $Arrow(C)$. Then this can be defined as a category whose objects are morphisms of $C$ and whose morphisms are pairs $(f,g)$ of morphisms that form a commuting diagram, but I feel the more categorical approach is to construct this using the functor category $Hom(T_2,C)$ so the arrow categories framework has been rewritten to be this way. In particular, the to-natural-transformation method can be applied to morphisms in arrow categories.
• In the same vein of making things more categorical, I have become a fan of Lawvere metrics. The distances framework is now based upon them, and $\mathbb{R}^{\infty}_+$ enriched categories. Distances should be studied by reference to certain types of enriched categories.
• I have provided support for cones and cocones as special types of natural transformations. This should be make the categorical implementation of limits/colimits easier. Set cones and cocones are also special types of morphisms of presheaves.
• The entire implementation of functors and presheaves in this program had to be changed on a basic level to help support structure presheaves. Functors are based upon the get-object and get-morphism multimethods while presheaves use the get-set and get-function multimethods. Structure presheaves implement both, so they are like functors and presheaves at the same time.
• I actually implemented section preorders using the section-preorder method. This is something I have talked about here but it wasn't converted into code until now. In the future this will be integrated with the category of elements of a presheaf.
• Among the first functors implemented in the structure presheaves framework are partial copresheaves which are functors to the category of sets and partial maps and relational copresheaves which are functors to $Rel$. I've known for a while that I would want to implement functors to $Rel$ but I didn't have a framework that felt quite right until now with the structure presheaves system. With structure presheaves everything feels quite right.
• Functors from monoids to the category of partial sets are now called PSets rather then PartialActionSystems because it always makes sense to abbreviate things you use a lot.
• We now have support for copresheaves of monoids and other structure copresheaves. The copresheaves of monoids will make way for other nice constructions like presheaves of abelian groups and presheaves of modules.

There is more to be done, but the one thing that remains clear is our strong committment to presheaf topos theory. Presheaves are the means by which we model computation.

Two aspects of the presheaf theory of categories

The topos theory of categories, and the idea of presheaf representations still requires further clarification. I think we can split up the presheaf topos theory of categories into two parts:

• The topos theory of the category of categories $Cat$ which is now provided by the topos of compositional quivers. This topos is defined by chaining appropriate quivers in a composition manner.
• The topos theory of a general category $C$ which is provided by the Yoneda embedding $F: C \to Sets^{C^{op}}$ which fully and faithfully embeds any category into its topos of presheaves.

So basically, the theory of compositional quivers which I have defined is actually part of the topos theory of the category of categories $Cat$ while the topos theory of Yoneda's embedding of categories is part of the theory of individual and specific categories. The Yoneda embedding produces a different topos $Sets^{C^{op}}$ for every category.

The usefulness of the Yoneda's embedding doesn't mean that the idea of presheaf representations shouldn't be further explored. For one we could study the different Yoneda's embeddings of categories and how they relate to Grothendieck topoi and their topological properties, which I now has been done before. For another thing, its still useful to consider presheaf representations aside from the Yoneda's embedding for various reasons.

In particular, when considering something like the presheaf representation of algebraic structures, in our topos theory of universal algebra, it is best to consider presheaf topoi over finite index categories. As an algebraic structure is constructed out of a finite number of sets and functions, it should be defined as a presheaf over a category with a finite number of objects and morphisms.

Using the appropriate presheaf representation can lead to easier computations, and so that leaves the issue open. Whenever we consider an algebraic structure, we should immediately ask what kind of presheaf is it. The kind of presheaf it is, is determined how its sets and functions are combined. So that is why categories belong to the topos of compositional quivers, as that topos defines the composition law which is that morphisms $m: A \to B$ composed with morphisms $n: B \to C$ should produce morphisms of the form $n \circ m: A \to C$.

These different little details are going to be important in our implementations. One thing is for sure: everything is a presheaf and presheaves (respectively sheaves) are the most important objects in algebra and geometry. Algebraic structures are presheaves, like how categories are presheaves in the topos of compositional quivers. Geometric structures are sheaves such as schemes.

References:
Yoneda embedding

The category of elements and section preorders

The category of elements of a copresheaf $F$ denoted $el(F)$ provides an algebraic context to the section preordering. In particular, we have that the section preordering on $F$ is just the object preordering of $el(F)$.

Proposition. let $F : C \to Sets$ be a copresheaf, then the object preordering of $el(F)$ is the section preordering of $F$.

This is useful because now we know that the section preordering of $F$ can be constructed from the object preorder of its category of elements. The subobject lattice of $F$ is then basically the Heyting algebra of the Alexandrov topology of open subsets of the section preorder.

See also:
Subobject lattices of presheaves

Congruence lattices of categories

Congruences are the most fundamental concept there is. For example, in ring theory we study congruences indirectly through ideals. Its unthinkable that such important structures as categories shouldn't have congruences define over them. Fortunately, we can solve this problem by embedding categories in an appropriate topos.

Background
A categorical congruence of a category $C$ is a unital-quiver congruence $(=_M,=_O)$ that satisfies the equivalent of a semigroup congruence on the composition operation of a category: \[ \forall a_1,a_2,b_1,b_2 : a_1 =_M a_2 \wedge b_2 =_M b_2 \Rightarrow a_1 \circ b_1 =_M a_2 \circ b_2 \] In other words, $((=_M)^2|_{D(C)},=_M)$ is a composition congruence where $(=_M)^2|_{D(C)}$ is the partition of the composition domain of $C$ induced by $=_M$. Then every such congruence induces a congruence $(=_M)^2|_{D(C)},=_M,=_O)$ of $C$ in the topos of compositional quivers.

Congruences of the two arrow category:
Consider the index category $T_2^*$ of the topos of quivers: Then it has a congruence lattice that looks like this: As a quiver is a functor on this category $T_2^*$, and every functor induces a categorical congruence, each of these congruences determine different types of quivers.

• The congruence that equates no objects and morphisms determines a generic quiver.
• The congruence that equates the source and arrow morphisms determines a coreflexive quiver. These are precisely the quivers whose underlying relations are coreflexive.
• The congruence that equates the object and morphism sets describes a quiver whose vertex and edge sets are the same.
• The congruence that equates the source and arrow morphisms and both objects determines a coreflexive quiver on a common set of edges and morphisms.
• The congruence that equates the source and identity morphisms makes it so that the source of each morphism is the morphism itself.
• The congruence that equates the target and identity morphisms makes it so that the target of each morphism is the morphism itself.
• The congruence that equates everything is a coreflexive quiver on a single set, where the source and target objects of a morphism are the morphism itself.

So the congruence lattice $Con(T_2^*)$ does tell us something interesting about this category, and the functors that can be formed on it. In the same way that the ideals lattice determines what morphisms can be sourced from a given ring. So for example, a homomorphism starting from a field must always be either trivial or injective because a field has only two ideals. This simple example fails to demonstrate the fact that the congruences of a category don't always coincide with the congruences of that category as a unital quiver.

Congruences of a total order on three elements:
Consider the three element total order $T_3$: Then its lattice of congruences as a unital quiver $Con(T_3)$ looks like this: On the other hand, its lattice of congruences as a category $Con(T_3)$ looks like this. Then its clearly smaller then its counterpart. In fact, the former has seven coatoms while the later has only four. So while it is note the case that the congruence lattice of $T_2^*$ is smaller for it as a category then as a unital quiver, in the general case the categorical congruence lattice is smaller because it has the extra condition of being a congruence of composition. It can clearly be seen:

Proposition. let $C$ with $Q$ its underlying quiver then $Con(C) \subseteq Con(Q)$ and $Con(C)$ is a meet subsemilattice of $Con(Q)$.

So categorical congruences are just defined from unital quiver congruences by the condition that compositions must be unique with respect the morphism partition. This makes them a subsemilattice of the unital quiver congruence lattice.

Congruences of the two pair category:
Consider a category with two different ordered pairs: Then its congruence lattice looks like this: Consider now the congruence that equates the objects one and two but no morphisms. Then this is certainly a valid congruence, for example we can define a monotone map from this thin category to $T_3$ that takes 0 to 0, 1 and 2 to 1, and 2 to 2 and as a monotone map that is a functor, and its underlying partition is a categorical congruence. However, consider the resulting quotient. Clearly it is not a category, because the composition of two arrows that have an intermediate object is not always defined.

Proposition. the quotient of a category by a congruence is not necessarily a category

Instead, the quotient of a category by a congruence is always a partial magmoid. Partial magmoids have no axioms that would prevent them from being closed under quotients, because any quotient of their binary operation is again a partial magma. So the category of partial magmoids is nicer then the category of categories $Cat$ in at least one way, but it is still not enough. The nicest categories are topoi.

The topos of composition quivers:
So we define the topos of composition quivers from a presheaf on the index category that looks like this: The relevant fact is that a category is essentially described by the data of three sets and six functions: the first, second, composition, identity, source, and target functions. This topos includes not only categories but all their generalisations like partial magmoids and beyond. Topos theory is the most advanced branch of mathematical logic we have available. Applying it to understanding categories can be very rewarding.

See also:
Congruence lattices of quivers

Locus 1.3.0

I published the next big version of Locus to github. It features the completed topos theory of categories based upon presheaf representations and compositional quivers. That is the main feature implemented in this new version. This is apparently original work, but once you think about it its pretty obvious there is no other way to thinking of categories except as presheaves of the compositional quiver type.

• Quivers, unital quivers, permutable quivers, dependency quivers, etc are all significantly improved so that you can run computations with their subobject and congruence lattices. Some of that has already been displayed here.
• Ternary quivers are now being implemented in Locus. These are like the familiar quivers used to describe graphs, except their edges have three arrows coming out of them. They are to a large extent responsible for the topos theory of abstract algebra, as binary operations are ternary quivers. Their three components are the first component, the second component, and the composite for any ordered pair. So magmas for example are ternary quivers.
• Categories are composition quivers, which are defined by a ternary quiver heading into a binary quiver consisting of morphisms and edges. The ternary quiver defines the composition binary operation of the category, and the composition of the underlying index category ensure that the ternary quiver operation is compositional on the binary quiver. This leads to the topos theory of categories, which is a great asset to us because it is best to think of categories as objects of a presheaf topos.
• By the same token we can study partial magmoids, which are the horizontal categorification of partial binary operations, magmoids, semigroupoids, groupoids, and all other related compositional structures via the topos of composition quivers. This justifies by implementation of these categorical algebraic structures in Locus, and my decision to consider them based upon topos theory to be special types of presheaves.
• Locus is going to be absolutely categorical. So for example, magmas will be magmoids, rings will be ringoids, ordered monoids will be two categories, etc. The only question is what type of structures you want to add on to a category. This new implementation of Locus sets the groundwork for that change.
• The next versions of Locus will study other presheaf related constructions on categories. The entire project is based upon presheaf foundations, and that now comes through by representing categories as presheaves.

Congruence lattices of undirected graphs

Locus can now compute the congruence lattices of undirected graphs using topos theory. This uses the topos of quivers with involution.

P3
Here is the path graph on three elements: Here is its congruence lattice: K3
Here is the complete graph on three elements: Here is its corresponding congruence lattice: P4
Here is the path graph on four elements: Here is its congruence lattice: S4
This is the star graph on four elements: Here is its congruence lattice: C4
Here is the cycle graph on four elements: Here is its congruence lattice: This congruence lattice is already getting quite big so we can stop this here. Rest assured that every undirected graph, and indeed every mathematical structure, has a congruence lattice defined over it even if we can't see it.

Total subobjects of quivers

Subobjects are categorically dual to quotients. In this context, if we were to dualize the idea of the lattice of thin congruences of a quiver, then its counterpart would have to be total subobjects. Let $Q$ be a quiver then a total quiver is one in which every object $o \in Ob(X)$ has at least one morphism going in to it $f : x \to o$ or going out of it $g : o \to y$. This produces the following duality:

• Subobjects: total subobjects can be determined from any morphism set
• Congruences: thin congruences can be determined from any output partition

The total function is an interior function on the lattice of subquivers $Sub(Q)$ whilst the thin function is a closure function on the lattice of congruences $Con(Q)$. We should always bear in mind that every concept in category theory has a categorical dual, so just as an object has congruences so too does it have subobjects.

See also:
Subobjects and quotients of thin quivers

External links:
Duality
Quivers

Object preserving congruences of quivers

Let $Q$ be a quiver. Then thin congruences are characterized by the fact that they are fully determined by their object partitions. It would be interesting to consider the dual case of partitions that collapse morphisms but no objects.

Theorem. let $Q$ be a quiver then its lattice of object-preserving congruences $L$ is equal to the direct product of the partition lattices of each of its hom classes: \[ L = \prod_{a,b \in Ob(Q)} Con(Hom(a,b)) \] Proof. let $P$ be a morphism partition for $Q$ and suppose that $a =_P b$ then since this is an object preserving partition, if $s(a) \not= s(b)$ or if $t(a) \not= t(b)$ that would imply that either $s(a) = s(b)$ or that $t(a) = t(b)$ with respect to the object partition induced by $P$, which would be a contradiction of the fact that this is supposed to be an object-preserving partition. So every pair of equal morphisms in $P$ must be parallel in $Q$.

Parallel pairs of morphisms are contained in hom classes $Hom(a,b)$ for pairs of objects $a,b \in Ob(Q)$. It follows that for any morphism $m : a \to b$ the only other morphisms it could be made equal to our those in $Hom(a,b)$. So its part of a congruence lattice $Con(Hom(a,b))$. Then consider all the hom classes of the quiver $Q$, they all have partition lattices that direct product to the set of all object-preserving partitions of $Q$. $\square$

We saw in the theory of thin congruences that the thin congruence associated with any object partition is in fact its equivalence maximal member. So this allows us to characterize the bounds of the lattice of object preserving congruences:

Corollary. let $Q$ be a quiver and let $L$ be its lattice of object-preserving congruences. Then its equivalence minimal member is the trivial partition which equates no elements, and its equivalence maximal member is the thin congruence.

This allows us to better characterize the relationship between thin congruences and object partitions. As we saw here, both thin congruences and object preserving congruences can both be characterized in terms of partition lattices. However, the same is not true for the lattice of congruences $Con(Q)$ of a general quiver $Q$ which need not have any familiar structure in terms of partition lattices.

References:
Quiver in nlab

Subobjects and quotients of thin quivers

Thin quivers are an important special case in presheaf topos theory. Suppose that we have a thin quiver $Q$ then we can form and consider its subobject and congruence lattices $Sub(Q)$ and $Con(Q)$ normally, but far more interesting is to consider subobjects and congruences of a thin quiver that remain thin.

Theorem 1. let $Q$ be a thin quiver, then every subobject of $Q$ is thin.

Proof. Thinness is a non-existence condition stating that there do not exist morphisms $m: A \to B$ and $n : A \to B$. Non-existence conditions are subset closed. $\square$

It is rather trivial that thin quivers are subobject closed, and that the subobjects of thin quivers are again thin. Of course, it also follows that any subcategory of a thin category is again thin. Far more interesting is the case of congruences of quivers that have thin quotients.

Lemma 1. let $Q$ be a thin quiver. Then $Q$ has no congruences that collapse two morphisms $m: A \to B$ and $n : C \to D$ without also equating two objects. $Q$ has a unique object-preserving partition.

Proof. $Q$ is a thin quiver it therefore follows that for the two morphisms $m$ and $n$ we must have either $A \not= C$ or $B \not= D$. Suppose that $A \not= C$ then we would have to equate $A$ and $C$ under the congruence so that would produce an equal pair of objects. Likewise, if $B \not= D$ then we would have to equate $B$ and $D$ also producing an equal pair of objects. So no two non-parallel morphisms can be equated under a thin quiver congruence. $\square$

This is the base case, which is that there is a unique congruence for the object partition that preserves all objects. Our goal is to show that there is a unique quiver congruence associated to every object partition.

Lemma 2. let $Q$ be a quiver, then the equivalence minimal congruence that turns $Q$ into a thin quiver $Thin(Q)$ is the congruence that equates all parallel pairs of morphisms in $Q$ and no objects. All other morphisms $f: Q \to T$ from $Q$ to a thin quiver factor through $Thin(Q)$.

Proof. let $Q$ be a quiver. Then in order for $Q$ to be thin there must not be any pairs of morphisms $m$ and $n$ with the property that $s(m) = s(n)$ and $t(m) = t(n)$. Thusly, to make $Q$ thin we can equate all such pairs of morphisms $m$ and $n$ to get the congruence $Thin(Q)$. This has as a quotient a thin quiver because it can not have any pairs $m$ and $n$ with $s(m) = s(n)$ and $t(m) = t(n)$ for if it did it would contradict the fact that we collapsed them. Then to see minimality, consider that any other congruence $C$ of $Q$ must also collapse all such pairs $m$ and $n$. It follows that $Thin(Q)$ is the minimal thin congruence. $\square$

With these two lemmas we now have have the means we need to prove our main theorem, which is that the thin congruences of a quiver are fully determined by object partitions.

Theorem 2. Let $Q$ be a quiver and $B$ a partition of its objects. Then there is a unique quiver congruence of $Q$ with $B$ its object partition that has a thin quotient.

Proof. there is always a unique quiver congruence associated to any object partition $B$ of a quiver $Q$: the congruence that collapses all objects in $B$ but no morphisms. We can always form this congruence by the pair $(id,B)$. Then the quotient of this congruence need not be thin. So by lemma 2 we can form a partition $A$ of the morphism set $E$ by equating all parallel edges which turns $\frac{Q}{(id,B)}$ into a thin quiver. This forms the following commutative diagram: Then also by lemma one, we see that every morphism from $Q$ to a thin quiver $T$ that goes through $B$ must filter through $\frac{Q}{(A,B)}$. However, by lemma one we know that no such further congruence can exist without further equating the objects of $B$. So $\frac{Q}{(A,B)}$ is the only thin quiver produced by a congruence with object partition $B$. It follows that thin congruences are fully determined by their object partitions. $\square$

If by theorem 2, we have that each object partition is uniquely associated to a thin congruence, then there is a one to one mapping $U : Con(Ob(Q)) \to Con(Q)$ that maps any object partition into a thin congruence.

Corollary. let $Q$ be a quiver then the suborder of $Con(Q)$ consisting of all thin congruences is isomorphic to the partition lattice $Con(Ob(Q))$ of partitions of the object set $Ob(Q)$.

It follows from this that the lattice of thin congruences of $Q$ is simply a partition lattice. We can further consider the thin mapping we defined in lemma 2 to be a closure operation on $Con(Q)$.

Corollary. $Thin: Con(Q) \to Con(Q)$ is a closure operation on the lattice of congruences of a quiver $Con(Q)$ that maps any congruence to its thin component.

The relevance of this result is that we can understand the epi-mono factorisations in the full subcategory of the topos $Quiv$ of thin quivers. We see from this that every morphism of directed graphs is determined by a vertex partition on the one hand a subset of vertices and edges on the other. The interesting thing about this is that it produces a dichotomy between congruences and subobjects, where only the later requires both object and morphism components.

Of particular interest is the application of this theory to considering subobjects and congruences of binary operations, which can simply be considered to be quivers with an algebraic function operation adjoined to them in the topos $Sets^{T_{2,3}}$ of ternary quivers. This leads into a more advanced topos theoretic theory of algebraic operations and their subobjects and congruences, which will be helpful in defining the topos theoretic foundations of algebra.

We see that topos theory provides the best foundation for combinatorics because topoi like $Quiv$ let you reason logically about graphs, digraphs, etc. $Sets^{[1,2]}$ lets you reason about hypergraphs. In order to make it the best foundation for abstract algebra we need to consider other topoi like $Sets^{T_{2,3}}$. In order to use topoi in geometry, as was originally intended, we can consider topoi of sheaves $Sh(X)$ of topological spaces. Every branch has its own topoi available for further study, which makes topos theory such an exciting field for further research and analysis.

References:
Quiver in nlab
Topoi: The Categorial Analysis of Logic

Congruence lattices of quivers

Let $Q$ be a multi-directed graph, then $Q$ is associated to a lattice of congruences $Con(Q)$ which can be constructed using new and original algorithms of mine. A quiver can be seen as a presheaf over the following category: This category I call the double arrow category, because it has a repeated pair of arrows going from the first object to the second one. As a category, it has an underlying quiver $Q$. Its congruence lattice $Con(Q)$ looks like this: This defines the congruence lattice of a multi-directed graph, but the same could be applied to any directed graph without repeated edges. Consider the directed cycle graph $C_3$ on three elements: Then the congruence lattice of the directed cycle graph $Con(C_3)$ has this interesting structure: This different sort of congruence lattice for $Con(C_3)$ might look unexpected at first, but actually it makes perfect sense. It is formed by adjoining two different five elements congruence lattices of a three element set to one another. Recall that the congruence lattice $Con(S)$ of a set with three elements has the structure [1,3,1] and that it has five elements. The reason for this appearance is that the cycle $(0,1),(1,2),(2,0)$ has this unique property is that every vertex is in any two of its edges. Therefore, in order to form any congruence of $C_3$ you must first collapse all of its vertices.

We have shown that every directed multigraph is associated with a congruence lattice $Con(Q)$, but let us not forget that every object of a congruence lattice is associated with a quotient. In the case of $C_3$ all of the different congruences of the same size and height have the same quotient, and so all the different quotients of $C_3$ can be formed one after another. They are formed in five steps: starting with $C_3$, collapsing a pair of objects, then collapsing another pair of objects, then collapsing a pair of morphisms, then collpasing the last pair of morphisms.

We have now seen the congruence lattice $Con(C_3)$ of a directed cycle graph on three elements as well as all of its quotients. It had the unique structure of a weak order. It would be interesting to see if $C_4$ has the same structure of congruences: Then the congruence lattice of $Con(C_4)$ looks as displayed below. It does not have the property that it is two partition lattices adjoined to one another, because it doesn't have the property that any vertex is contained in any pair of edges. Nonetheless, you still have to collapse at least three objects before you can collapse one edge, so you can still visibly see the fifteen element partition lattice on four elements on the bottom connected to another one above it but now with some mixed congruences between them:

Another directed graph with an interesting congruence lattice is the strict total order $T_3$. It has a congruence lattice $Con(T_3)$ as displayed below. The reason for this interesting structure is that when you collapse two lower objects you then get repeated edges from the lower class to the upper one. These repeated edges can then be collapsed without equating more objects, and the same works in the other direction from above. So you get this interesting self dual structure in the form of a lattice. We have considered some interesting cases of directed graphs, but what if you have a repeated edges. In that case, we can see that repeated edges actually do have an effect on the appearance of the congruence lattice. A directed multigraph with repeated edges has as an atomic congruence a partition that equates two parallel edges rather then two vertices. So the atoms of such a congruence lattice don't necessarily generate a partition lattice, so they appear different. This is a non-thin quiver, so it has an atomic congruence that is not part of any partition lattice. It is the unique atom that is not a part of an element that covers three atoms. Consider two disconnected edges: Then their congruence lattice is displayed below. Initially, it just looks like a partition lattice on four elements, but there is a little bit more that meets the eye. There is one special congruence on the disconnected pair of edges: the one that equates both the minimal edges and that equates both the maximal edges. Then the two arrows can also be equated to get a parallel pair between two objects as a quotient. The disjoint arrows map is a function, but it is perhaps not a transformation because it is not closed. But we can make it one like this: Simply adding these two edges creates a much larger congruence lattice, which demonstrates how these congruence lattices tend to grow quite large for even small directed graphs: Topos theory generates congruence lattices for far more objects then classical lattice theory, which would only generated them for lattices or semilattices. We can now generate them for any poset. Consider the following poset: This poset is known as $[1,2]$ and its congruence lattice $Con([1,2])$ is of the following form: These congruence lattices are already getting quite larger. We can certainly go deeper, and create congruence lattices for even larger directed graphs and we can even run computations on them, but they will get too big for Graphviz to display nicely I think so we'll have to leave it at this. The congruence lattices generted so far should give you an inkling of the subject.

All these congruence lattices were generated by using the topos $Quiv$. This is just a small sampling of what can be done with topos theory, within only part of one subject. Topos theory is a logical theory of everything, and its techniques are the most widely applicable.