Можно выбросить все диаграммы, если хочется, как в виде рисунков, так и в любом другом. Останутся только морфизмы с равенством, и ничего по существу не изменится. Так пойдёт?

А диаграммы не подчиняются законам логики?

Категориальная логика -- это крупные элементы категорий на базе логики, а не наоборот.

Насколько я понимаю, к обычным формулам и правилам вывода добавляются пруф-теоретические элементы, уже в которых мы имеем категории.

Просто приведу один пример. Есть такое утверждение, что любая инъекция Prop -> Prop является биекцией. Его можно доказать на логическом уровне, не используя никаких диаграмм, а можно на категориальном. Второе доказательство есть в слоне, например. По сути это два одинаковых доказательства, написанных на разных языках.

Категориальная логика как раз и связывает эти два языка и показывает как перейти от одного к другому.

Это выходит за рамки разговора про логики как внутренние языки категорий?

Нет, это как раз одна из двух частей этого соответствия.

что такое "слон"?

Просто приведу один пример. Есть такое утверждение, что любая инъекция Prop -> Prop является биекцией. Его можно доказать на логическом уровне, не используя никаких диаграмм, а можно на категориальном. Второе доказательство есть в слоне, например. По сути это два одинаковых доказательства, написанных на разных языках.

Sketches of an elephant

Ок, т. е. вся категориальная логика про это, да?

Ну более-менее

Здорово, спасибо

у шульмана есть неплохое введение http://mikeshulman.github.io/catlog/catlog.pdf

Диаграммы, это просто способ записывать равенства.

True

Ну это я какбе к вопросу о "диаграмм в логике не бывает" ;-)

По категориальной логике на русском самое лучшее, что видел, это от Васюкова.

Ну, lambda-исчисление -- оно же тьюринг-полное, поэтому можно считать, что все базовые формы данных (скажем так) являются специальными лямбда-выражениями. Но вообще, в любом моноиде Чёрча живут, естественным образом, типы -- это идентпотентные морфизмы, которые t после t = t, на них можно строить уже разнотипную ДЗК. Как-то так и происходит на практике, мы же умеет компилировать типизированный Haskell в нетипизированный ассемблер.