Которую мы сохраняем

кстати, а как решать эту задачу корректно? Вот мои наброски:

Set^K = K -> Set
теперь давай посчитаем, сколько можно построить таких функторов (к счастью, мы не ограничены естественностью, так как из стрелок только единичные). Каждый функтор можно представить парой из двух множеств (на этом доказательтство можно заканчивать вроде), где первое множество - кодомен из A, а второе - кодомен из B, значит |K -> Set| = Set^2 (ну и видно что K = 2), значит количество объектв одинаково. Количество стрелок тоже одинаково, так как у нас есть стрелки, меняющие множества в паре (и там и там)

Ну мне кажется, что все норм, я бы тоже ограничился фразой: каждый функтор из Set^K представим как пара множеств из Set x Set

В категории категорий стрелки — функторы.
Функторы можно назвать гомоморфизмом категорий.
Они сохраняют структуру категорий.
Ну а дальше всё обычно про изоморфизм.

Хотя и в целом, изоморфизм категорий, это слишком сильное свойство, которое редко используется.
Чаще говорят про эквивалентность категорий.

А как различить? Вот в примере выше — изоморфизм или просто эквивалентность?

У нас есть биекции объектов и морфизмов, нужно ли что-то ещё?

Из изоморфизма следует эквивалентность.

https://en.wikipedia.org/wiki/Equivalence_of_categories
Если я правильно понял вопрос, там есть ответы.

Биекции объектов и морфизмов — это слабое свойство.
Нужно, чтоб были _функторы_.
И уже про функторы можно всякия условия говорить.

Вроде функтор биективный на морфизмах автоматически будет изоморфизмом.

Будет.

только следы, что он работал в этом направлении, но "печатных" результатов нет
http://www.math.miami.edu/highlights/events/lecture-series-by-v-voevodsky/
http://www.mathnet.ru/php/seminars.phtml?option_lang=eng&presentid=1694

> mathnet.ru
Да, я это видео и имел в виду.

http://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Probability/Singletons/Stage_2/singletons_current.pdf
есть вот такая статья

The goal of this paper is to solve the following problem.  Consider a population of identical ageless individuals (singletons) where each individual can go through one of the two possible transformations - it can die or it can divide into two. Suppose that the past history of the population was determined by the conditions that the birth (division) rate was constant and equal to 1 and the death rate was an unknown function of time d(t).  Suppose further that we know the ancestral tree of the present day population, i.e., for each pair of singletons we know the time distance from the present to their "last common ancestor".  Given this data what is the maximal likelihood reconstruction of the death rate function?

я её не читал, категории в статье есть

о, а ещё такое есть
http://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Probability/Stochastic%20Categories/Stage4_2008_08/markov_current.pdf

Notes on categorical probability

обе статьи нашёл вот здесь http://www.math.ias.edu/Voevodsky/voevodsky-publications_bib.html

А вот такой полупрактический гипотетический вопрос.
Представим, некоторый язык или proof assistant, в котором нет завтипов.
Есть totality checker, какое-то равенство для любых типов, индуктивные типы, которые определяются с использованием не только суммы и произведения, но также эквалайзеров и коэквалайзеров.
Иными словами при определении типа данных я могу снабдить его свидетельствами равенства или классами эквивалентности.

Позволит ли такая форма зайти хоть куда-то в доказательствах? А если заменить (ко)пределы (ко)концами?

Автоматическое доказательство уже невозможно.
А богатства термов для их написания этих доказательств недостаточно.
Как-то так.
Как минимум, хоть какие-то зависимые типы должны быть.
В принципе, это может быть _один_ зависимый тип равенства стрелок.
И им уже дальше можно описать многое остальное.

Хватит одного зависимого типа или нужен весь этот инфинити группоид?