Catecon: Visualizing Coherence In The Categorical Console

Videos for the Categorical Console.


Up to “Hello, world!”

“Now, Bob,” I distinctly recall Saunders saying to me.  “You have to have good names for your ideas.”

I had gone in for our weekly meeting to complain about one of his names, namely that of “central morphisms”.

I opined that the “centrality” should extend through the entire hierarchy of the domain and codomain shapes, and not just the top-level factors.

Of course, I never called him Saunders.

And my name is Harry, not Bob.

Even though I didn’t look much like a popular war hero senator from Iowa, Bob Dole at the time was running for President and I became “Bob”.

Mac Lane set me to the task of looking into symmetric monoidal closed coherence and noted in his memoirs that I never published.

That time he got my name right.

He knew I was into computing, although what I did about it while at Chicago wasn’t too shareable with him.

Well, they didn’t have any computer science department after all.

Here I’ll show how I visualized coherence and computation in those days.

As one classmate stated walking out our shared office door while staring at my colored chalkings, “that’s not math.”

Later he wandered off to the Economics department and took cohomology with him.

Not sure how that worked out.

For background references if you’d like to read ahead, on there are two articles, one “Intro to Categorical Programming” and another “V is Vortex:  More Categorical Programming”.

The articles reveal how techniques like those to be shown here were used thirty years ago to make the Clipper microprocessor.

The categorical editor in those days was a whiteboard.

We’d draw a diagram on the whiteboard and translate the composites and whatnot into the command language.

Programs often worked first time like a charm and frequently faster than custom C code at the time.

This attempt, unlike thirty years ago, does have a graphical editor, and that is Catecon, the Categorical Console.


Good, what’s a category and why do we want to console one.

For a console, a way to easily build up composites and universals in a category is the goal.

Many watching this already know what a category is.

For others, the Categorical Console builds up your categorical intuition so stay tuned.

When I learned Category Theory as a kid, I felt my brain being rewired like when I had earlier learned touch typing.

Perhaps some feel the same.

Since categorical work showing arrows for morphisms and forming diagrams is common practice, that approach is taken here and becomes the essence for the editor.

We select a category to do our baseline computations.

Partial Finite Sets: PFS

Catecon starts in the category Partial Finite Sets or PFS.

The choice for finite sets is due to current hardware limited to a finite realm (and presumably universes, but that’s a touchy digression).

Since we do finite work, let’s do it in finite sets.

The “partial” part is due to how to define the computations.  More later.


Diagrams are the collections of objects and arrows we draw.

These are functors or morphisms of their own from a finite category to some category of interest.

When satisfied, one submits diagrams to Catecon to share with others.

Catecon is then a store of diagrams for shareable, executable, math.

We start in the draft diagram where we may scribble away.

The draft diagram for playing in has a preset list of reference diagrams.

We start with placing objects in our diagram.


Objects in categories are those things we wish to manipulate.

For basics we have the initial object (all objects come from it) and terminal object (all objects go to it).

These represent the empty set and one-point set.

Any object we have in PFS is essentially some generic finite number.

For arithmetics, we have various numerical objects like the natural numbers, integers, and (cough) floating point numbers.

Though we think of the natural numbers and integers as infinite, we’re constrained in PFS to have some model that works somewhat like what we want.

Floating point numbers are, well, spit, non-Archimedean.

We have other compound forms of these elements with products and coproducts.

We drag these and drop them on our diagram to instantiate them.

We make a new object by specifying its name, some code, and HTML code entities to give a name.

Let’s create a generic finite object A.

But it seems like we cannot do much with these objects by just staring at them.

Let’s connect them.


Objects are best described by what morphisms are attached to them.

After all, you could not figure out what to do with an object unless you had a morphism to morph it to itself or another object.

We have some reference diagrams that show available morphisms.

In basics, we have the unique morphism from the initial object to the terminal object.

That is just the unique function from the empty set to the one-point set.

In the first order logic diagram, we see true, false, negation, equality, and, and or.

For arithmetics, we see the special numbers zero and one, and the typical operators one expects like addition, successor, and predecessor.

What to do first?

Clear the screen.

Hello, World!

The vernaculars start with some form of “Hello, world!” to show they take your code and produce a runnable output.

In our case with a web browser, we’d best come up with some form of a TTY console.

We also need strings.

Look at the reference diagram Strings to see what we can use.

In this diagram, Str represents the space of all strings.

Well, as much we we’d like all strings, or all the strings you can represent on your box, this space may better represent all the strings in this effort before your browser shuts down.  And that’s a finite set.

We need to take an element of string space to have a given string.

Drag Str to our diagram.

Same for the object one.

Control-drag from the object one, the one-point set, and you see an identity morphism form.

Hover the codomain on the Str object and the codomain turns blue.

Drop the object on Str and we have formed a morphism from the one-point set to string space.

Selecting the morphism gives us a chance to edit it.

Now we add data.

Given a one-point set domain, our index must be zero.

Now in the diagram Console, there’s a morphism from Str to tty.

Drag that to the diagram.

Pick up the Str and drag it to the other one and fuse it.

Given one morphism following another, what better to do than make a composite.

Select the first morphism, and the following morphism with a shift-click.

We see the composite icon appear.  Click it.

The composite appears between the very first morphism’s domain and the last one’s codomain.

In this case, since we start with a determined domain, an icon appears to run the composite.  Click it.

On the TTY panel we have our expected result, “Hello, world!”