Ну так а зачем? В конечном счёте, чтобы упрощать некоторые категорные доказательства, и пользы для собственно логики от этого нет, разве что очень косвенная

Чтобы можно было пользоваться категорными доказательствами прямо в логике при построении теорем.

А можно пример, где такое делают?

Насколько я понимаю, именно для этого делают, когда это интересует именно логиков. Самый лучший учебник по категорной логике на русском написал Васюков, можете попробовать посмотреть там.

Плюс, отдельно от всего этого, в логику могут быть встроены некоторые элементы теории категорий в модель вплоть до получения категориальных семантик, но я не уверен, что это называется категориальной логикой.

Напомните точное название, пожалуйста?
Или ссылку или даже книжку прям сюда, если несложно?

Так и называется же, "Категорная логика"

Пасиб.

еще вопрос из разряда самых основ. Читаю Бартоша про моноиды, и там рассматривается множество натуральных чисел с нулем. Окей, тут все понятно, ноль - нейтральный элемент, mappend на таком моноиде возвращает adder для инкремента аргумента на любое предварительно указанное значение. Окей, тут все понятно.

Дальше происходит плавный переход к тому, что моноид - это категория из одного объекта, а весь бесконечный спектр возможных аддеров - его морфизмы. У меня вопрос - почему это один объект?

Бартош говорит "ну ведь hom-set M(m,m) всегда определен, т.к. всегда можно сложить два числа и получить результат". Ну да, но и что с того?

я не понимаю, почему "любое число" стало одним объектом в категории, если мы абстрагируемся от типов, значений и всего такого. Или не абстрагируемся?

т.е. когда мы говорим про категорию-моноид на натуральных числах, то имеется в виду, что в M(m,m) в данном m - это Nat?

потому что я думал о бесконечном количестве типов с ровно одним инхабитантом, т.е. тип 0 с единственным значением 0, тип 1 с единственным значением 1, и т.д.

Nat объект, Nat -> Nat морфизмы?

если каждый объект будет отдельным числом, то получится категория натуральных чисел?

Не получится, терминальный объект нужен

объект в этой категории - не число. он вообще здесь не важен и семантики не несёт

числа здесь - морфизмы, бинарная операция - композиция, нейтральный элемент - id

так тоже можно, но тогда имея
n -> m и m -> t вы должны уметь сконструировать n -> t
К такому роду категорий относятся, например, (пред)порядки на натуральных числах. Моноид для суммы так выразить сложно

Топосы - это алгебраическая семантика, и она популярна