See the diagram at https://catecon.net/d/hdole/category
The notion of category is fundamental, so how does one describe a category inside another category?
Catecon is a categorical console, so we need a good answer.
Most gloss over the definition and leave out detailing those ‘evident’ diagrams typically left to the reader or grad student.
Who has seen the full definition of an internal category?
We will.
Let’s get morphing!
What is internalization in category theory? Short form: convert quantifiers to universal constructions like pullbacks et al.
Longer story found at the cognoscente’s nLab in the link below.
In Catecon, so far that means only morphisms with no quantifiers are allowed. How to put a quantifier on a morphism in Catecon is a separate topic from this one.
Writing down a full internalization of some mathematical structure can be daunting
The internal definition of a category requires pullbacks due to the gluing requirement that to be composable one morphism’s codomain is followed by the next one’s domain.
nLab shows a definition of internal category with those pullbacks that can act as a guide.
We write down the classical, or Bourbaki, version of the definition of category along one side, and on the other the diagrams for internalization.
In as much there may be more classical details than expected, we will see how they are required by the internal version.
Now classically: Let D be something which has collections.
The word ‘collections’ is math buzz for I’m not going to tell you how big this thing is, like a set, proper class, or type.
In Catecon, though, this, too, is an arrow.
As our current categorical context is Cat, the category of small categories, place a category D.
For clarity, let us show that D is a member of Cat.
Let C zero and C one be two collections in D.
The C zero collection represents the objects and C one the morphisms.
We’re still in object mode so double-click to create objects in D.
In the proper name text box entering C colon zero turns the zero into a subscript.
Next is the objects of morphisms for our internal categories.
Classically: For every object in C zero there is a corresponding morphism in C one called the identity of that object.
Let’s create the morphism C zero id C one.
Every morphism of C one, has domain and codomain objects in C zero.
We need two morphisms from C one to C zero, called dom and cod.
Create them.
For every object in C zero, the domain and codomain of its corresponding identity morphism is that object itself.
We take a copy of id, and one of dom, fuse, create an identity on C zero, and fuse.
This triangle is known as a cell in Catecon, and generally comprises two chains of morphisms, called legs, with common domain and codomain.
In Category Theory, CTs like seeing commutative diagrams, meaning all cells have both their legs equal.
As presented in this case, Catecon has an engine known as an equator, or equator, that which equates.
Engine output is three valued: true, false, and I’m not quite so sure about that, as presented in our current situation with the unknown commutativity icon.
This then is our first assertion about an internal category, meaning we need to assert that the id morphism followed by cod is the identity on C zero.
Do so by selecting the unknown marker and introspecting.
We see the cell’s commutativity status as unknown and a list of icons, followed by listing of the cell’s two legs.
Click on the commutative icon to set the cell’s two legs to be equal.
This registers said assertion and the cell’s commutativity status changes accordingly.
Nominally CTs do not mark all commuting cells in a diagram with such a symbol and instead say ‘all the following diagrams commute’.
In Catecon we use it as a marker that something special occurred here.
You also get something to click on later if you want to change your mind.
Select the identity and notice you cannot delete or detach it.
That is due to the assertion having a reference lock on all the morphisms in its cell.
To remove the assertion hit the delete button.
Now do similarly for the cod morphism and make the assertion.
A composable pair of morphisms are two morphisms of which the first morphism’s codomain is the second one’s domain.
Well, that’s just what we see all over the place in our diagrams, but here we need to formalize it.
Take our dom and cod morphisms and fuse C zero.
Select cod first followed by dom.
We now have an action to form the pullback cod by dom.
Pullbacks, or fibrations for the geometrically inclined, may somewhat be thought of as the subset of the product that satisfies that all paths commute.
In this case we get the object of composable morphisms along with its two projections to C one and commutative cell.
For this commutative cell we see the pullback icon to indicate something special happened here.
Define composition of two composable morphisms as an operation that produces a single morphism.
Copy our pullback object down along with the morphism object C one and make a morphism between the two called ‘comp’.
The domain of the composite is the domain of the first morphism in the composable pair.
Take a copy of comp and dom and arrange as the upper leg.
Take a copy of dom, project off the pullback’s first factor, fuse.
Select the unknown cell and assert it.
The codomain of the composite is the codomain of the second morphism in the composable pair.
Now build similarly with the cod and project the second factor from the pullback, and assert.
That gets us to this part of the definition, but the associative law is going to take some lifting.
Let’s next do ‘the left and right units laws for composition of morphisms’.
Form all the composable pairs of an object’s identity as the first morphism in a composable pair, and another such collection with said identity as the second morphism of a composable pair.
Fair enough.
Let’s make a copy of our composable morphisms pullback.
On the left side take a copy of cod and an identity morphism on C zero and take their pullback.
From this C zero place the id morphism to C one and fuse.
On the opposite C-one create an identity and fuse to the C one on the original pullback.
Now select the zero-th projection, followed by shift-selecting the identity, and then cod.
Next add in the one-th projection, followed by id, and then dom.
Lastly, select the original pullback object of composable morphisms.
What we have essentially done is define two legs of a commutative cell and targeted a pullback object.
We therefore can make a pullback assembly to that latter object as indicated by said icon here.
Do so.
That gives us the lift between the two pullback objects representing our need to go from morphisms with a certain codomain to morphisms with the identity on that codomain.
And we get commutative cells all around.
On the right side we do a similar construction with a pullback of dom and the identity, and we can get the lift from objects and morphisms with that domain, to the identity on that object with those morphisms.
At this time, you can see why CTs want their diagrams clean by generally showing no symbol for commuting.
Click on the U key and a commutativity symbol shows for each hidden cell.
Hovering over each shows the associated cell.
Clicking on a cell and introspecting shows how it got that way.
With those two lifts we can now form the left and right unit laws.
For any object A and the identity one on A, and for any morphism f from A to B, then f composed with the identity on A is f.
Similarly for the identity on B that it composed with f is f.
Copy our two lift morphisms and place the comp morphism from the common codomain.
On either side project off the morphism object C one, fuse, and assert.
We now have our left and right identity laws.
To discuss associativity of composition, we need composable triples.
So, form the collection of composable triples in the form f, g, and then h.
Place our cod and dom morphisms thusly, and a copy of our composable morphisms, project off the second factor and fuse the domain of cod.
Select the vertical leg first and then the bottom, and now we form the pullback of composable triples in the desired form.
Next: From the composable triple above, form the collection of composable pairs g, h.
Copy our dom cod pair and form the ubiquitous pullback for composable pairs.
Above the cod place a copy of the composable pairs and project off the second factor.
Now place a copy of the composable triples from above and project off the pair and fuse, and project off the single morphism factor and fuse.
Select the top leg first followed by the bottom leg, and lastly select the composable pair.
Our legs commute so we can now form the lift between the two pullback objects.
It might bring some clarity as to what is going on by seeing the string graphs of the involved morphisms.
So, you see that the resulting morphism has the stringy effect of giving us the desired g and h.
Now for the backbone of associativity.
From the collection of composable triples above, form the collection of composable triples in the form of f, then g, h.
Copy the dom and cod, add the composable pairs, and project.
First select the cod and then as another leg the projection followed by dom, and take the pullback.
This gives us the composable triples in the form f, then g h.
Copy the prior composable triples object and project off the pair and fuse.
For the other side, take the lift obtained in the prior diagram.
Select the upper right leg followed by the lower leg, and then the pullback object.
We can now form the lift between the two objects of composable triples.
Next up the legs of associativity.
From the first composable triple above, f, g, then h, form the collection of f composed with g, and h.
Take our primordial pullback and place the comp morphism as such on the right.
Place the composable triple f g then h and place its two projections.
Select the upper leg followed by the lower and then the pullback object.
And lift.
Correspondingly for the other leg: From the second composable triple above, f, then g, h, form the collection of f, and g composed with h.
Now we’ve done our pullbacks and lifts.
Before we do associativity let’s compare with nLab.
Here we have our primordial pullback though with differing proper names, and the projections start indexing from 1 rather than 0.
The next few diagrams have pi for projections, and they seem to be uniquely labeled versus Catecon’s local proper names.
The upper leg of this pullback suggests that the last morphism’s target, or codomain, is the same as the composed pair source, or domain.
Oh, dear.
In our case we have the dom and cod interchanged to glue the composable pair to the single factor.
Oh, well.
As said, who has seen?
Now for our final assertion: Composition in a category is associative if the composites of f, then g, h is the same as the composite of f, g, then h.
Select our backbone of associativity and place it thusly.
Now from those two objects place the two lifts we just made accordingly.
From those two codomains proceed with placing the composites.
Assert.
We now have all the assertions required for the definition of internal category.
In Catecon, a blob of connected morphisms is referred to as, well, a blob.
To make a definition in Catecon, select something on each blob or the assertion itself.
In our case, control A selects everything since we want it all.
Click the definition action.
Catecon scans the selected blobs looking for assertions.
Selecting the pullback and lift blobs do not add anything to the definition as they are inherent in the blobs for the assertions.
You see listed the required morphisms for this definition: comp, id, cod, and dom.
Pay no attention to the quantifiers.
In our case, there are seven assertions in the proposed definition.
Hovering over them emphasizes them in the diagram.
Call our definition ‘category’ and create it.
With our definition in hand, we can then create definition instances of it in any collective scope by providing the required morphisms and proving the assertions to be correct for those substituted morphisms.
Quod erat demonstrandum.
Internal definition of category in Catecon.