Так. Ребята. Я не так давно заметил одну достаточно простую вещь и мне показалось, что она может быть связана с условной теорией типов, в которой я совсем не разбираюсь. Ну показалось "на глаз". Вот типа есть у нас 2 изоморфных объекта в категории. Тогда множества Aut(A), Aut(B) и Isom(A,B) будут во взаимно-однозначном соответствии друг с другом. Какая-то интуиция из сферы, что я указал есть? Или вообще не в ту сторону пошел?