Но что вообще означает «одинаковые» для абстрактных морфизмов?
Возьмём контекст проще: аксиоматика группы. Что означает «одинаковые» для абстрактных элементов группы?
-- Сб сен 16, 2017 01:25:43 --Всё! Есть только три символьные формулы, каким-то магическим образом определяющие «равенство».
Можно было бы так говорить, но обычно такое больше смысла говорить об остальных символах кроме равенства, потому что подразумевается, что равенство и подстановка вполне конкретным образом связаны. Например, пусть

. Тогда вы совершенно точно знаете, что

и что если

обладает каким-то свойством, то и

им обладает. Это не следствия каких-нибудь
собственных аксиом теории категорий, это следствие (схем) аксиом конкретно равенства:
(1) рефлексивность:

;
(2) подстановка в термы:
![$x = y\to t[x/z] = t[y/z]$ $x = y\to t[x/z] = t[y/z]$](https://dxdy-01.korotkov.co.uk/f/8/0/8/808e2502f1f18db94f88b4f3da26ed1c82.png)
;
(3) подстановка в формулы:
![$x = y\wedge\varphi[x/z]\to \varphi[y/z]$ $x = y\wedge\varphi[x/z]\to \varphi[y/z]$](https://dxdy-01.korotkov.co.uk/f/8/1/9/819199d1aa2e823b5f1f1e3be60fc51482.png)
;

— переменные,

— терм,

— формула.
(В любой конкретной теории можно ограничить термы и формулы схем (2) и (3) атомарными, ничего не испортив, но это уже немного оффтоп. Также будет им, видимо, замечание, что если формализовать теорию категорий как двусортную (термы-объекты и термы-морфизмы), будет наложено естественное ограничение на подстановку терма вместо переменной, когда их сорта не совпадают. И вообще я не уверен, что вы готовы к такому низкоуровневому обсуждению. Но подобные вопросы о равенстве его почти требуют.)