[FOM] two interpretations of identity morphisms in category theory

[Patrik Eklund]

We shouldn't speak about 'objectual' and 'algorithmic' interpretations 
of the identity morphism.

The foundations of category theory has been debated since its beginning, 
and I won't go into detail in this response.

However, through decades there has been discussions about which comes 
first, objects or morphisms. Traditionally we train students saying 
"these are the objects, and the morhpisms are ...". However, if we look 
back e.g. at Ehresmann et co's algebraic view on categories dating back 
to the 1950s, there are notions of identities where seemingly morphisms 
precede objects. It appears implicitly in Menger's paper's from that 
time, so even Newton had some intuition of "identity" which is not 
overwritten today in any way, I would say.

---

Paul Hollander appears to include "the logic of it" aspects to morphisms 
and objects, but it is important to note that we shouldn't neglect any 
of algebra, logic and topology influences to category theory.

On algebraic aspects, note e.g. how we have algebras and co-algebras, 
where the former is closer to dealing with Eilenberg-Moore categories of 
monads, whereas co-algebras go in direction of substitutions and Kleisli 
categories. An interesting thing is also if algebraic structure (in 
category theory) resides in objects or in morphisms. It may even be seen 
as a matter of choice, which we can see e.g. with playing just with 
categories of relations, which can be defined algebraically and 
co-algebraically. An additional algebraic abstraction enters the scene 
in monoidal categories. Here we should note that there is no notion of a 
free monoidal category (there are 'free categories', but that's another 
thing), so "categorical algebra" is not subsumed by "universal algebra".

Logic aspects of catagories are many. There is the "fons-et-origo" logic 
intertwined with set theory which appears in the metalanguage of 
categories. We have toposes and internal logic, and we have categories 
of logics in the style of institutions (Goguen-Burstall) and entailment 
systems (Meseguer). The latter can be generalized as can be seen under 
GLIOC (www.glioc.com).

Topologies seem a b it far fetched but to me an important question is 
related to "structure or space?". If we again use monads as examples, we 
have coarse structures starting from adding stuff to relations. The 
Kleisli category of the powerset monad is one of the to relational 
categories (in some sense the "wrong one" since it emphasizes 
substitution in the morphism rather than in the object), and the 
Eilenberg-Moore category of the powerset monad is (isomorphic to) the 
category of complete lattices and join-preserving maps. This intuitively 
shows that as we add more structure to the functor in that monad, we 
also add more algebraic structure to the corresponding Eilenberg-Moore 
category. What is interesting is the folklore "algebra and topology 
meet" in the case of the ultrafilter monad. The "algebraic structure" of 
its Eilenberg-Moore category is compact Hausdorff spaces.

So, adding stuff to (algebraic) structure is not the same as adding 
stuff to (topological) space. Here we might then wonder is a logic is a 
structure or a space. I personally tend to see it more as a space than 
many others do, but I wouldn't say "logic is all about space".

---

My remarks above may underline that we shouldn't separate algebra, logic 
and topology from each other, and definitely not without justification 
say that one is more foundational than the other.

What I would like to say also is that we mustn't forget "old papers and 
writings". If we rely too much on papers and books no more than a couple 
of decades old, we probably lose lots of stories.

FOM is very fascinating!

We are living interesting times!

Best,

Patrik


On 2017-04-29 22:22, Paul Hollander wrote:

> In category theory, the identity morphism 1x:x → x is ambiguous as
> between an objectual interpretation and an algorithmic interpretation.
> 
> Objectually, '1x:x → x' refers to the morphism 1x such that 'x = x' is 
> true.
> 
> Algorithmically,  '1x:x → x' encodes the algorithm by which premiss |-
> (x = x) implies conclusion |- (x = x).