[FOM] two interpretations of identity morphisms in category theory

[Paul Hollander]

Perhaps this observation is self-evident to practicing mathematicians, 
but to me (a philosopher with an interest in the foundations of math) it 
was not.

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).

The algorithmic interpretation is highly non-trivial when 1x is 
expressed as '1x:y → z', because this is interpreted as encoding the 
algorithm by which |- (x = y) implies |- (x = z).  On this approach, 
'1x:y → z' encodes inferences about x using 'y' and 'z'.

I'm curious as to feedback, favorable or not, from FOM.

Cheers,

Paul Hollander