21 июля 2026
22 июля 2026
25 июля 2026
27 июля 2026
Так. Ребята. Я не так давно заметил одну достаточно простую вещь и мне показалось, что она может быть связана с условной теорией типов, в которой я совсем не разбираюсь. Ну показалось "на глаз". Вот типа есть у нас 2 изоморфных объекта в категории. Тогда множества Aut(A), Aut(B) и Isom(A,B) будут во взаимно-однозначном соответствии друг с другом. Какая-то интуиция из сферы, что я указал есть? Или вообще не в ту сторону пошел?
Nikita RepeevЕщё можно такое сказать
Пусть f из Isom(A,B)
Тогда для любого g из Isom(A,B) найдётся такой h из Aut(A) что h = f;g^-1
Ага. Просто почему-то никогда об этом не думал.
Nikita RepeevЕщё можно такое сказать
Пусть f из Isom(A,B)
Тогда для любого g из Isom(A,B) найдётся такой h из Aut(A) что h = f;g^-1
Ну тогда можно сказать, что изоморфизм есть и рассматривать Hom, а не Isom.
Вооьще говоря, изоморфные объекты в категории на то и изоморфны, что не отличимы с точки зрения взаимодействия с внешним объектами. Мне было бы интересно, как корректно сформулировать фразу вида "истинность любого логического утверждения, возможно параметризованное каким-то объектами этой (да и другой) категории не зависит от представителя класса изоморфности"
Ну если утверждение это что-то пруф иррелевантное то два изоморфных типа дают в нем равные термы. В одну сторону легко.
А в другую это сказать что если типы не изоморфны то найдётся пропозиция которая их различит? В общем случае это кажется не обязано быть правдой, если мы внутренние штуки имеем ввиду.
28 июля 2026
Антон АбловВооьще говоря, изоморфные объекты в категории на то и изоморфны, что не отличимы с точки зрения взаимодействия с внешним объектами. Мне было бы интересно, как корректно сформулировать фразу вида "истинность любого логического утверждения, возможно параметризованное каким-то объек
Ну эта фраза просто часть определения категории в HoTT