OCaml версия книги "Category Theory for Programmers"

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

Ниже пример из Бартоша:

Моноид - операция && над Bool, нейтральный элемент - True, потому что:

True && True (as neutral) = True
False && True (as neutral) = False
True (as neutral) && True = True
True (as neutral) && False = False


Морфизмы - это сечения (в терминах Haskell) операции &&:
1) (&& True) - это функция-предикат над Bool
2) (&& False) - также

Затем я выписываю правила их композиции:
1) (&& False) * (&& False) = (&& False)
2) (&& False) * (&& True) = (&& False)
3) (&& True) * (&& False) = (&& False)
4) (&& True) * (&& True) = (&& True)

И таким образом, я могу выразить эту категорию, используя одни морфизмы:
f - False
t - True
^ - &&

Правильно ли я рассуждаю?

категории без объектов вроде не бывает, но рассматривать категорию над морфизмами какой-то другой категории нормально

это собственно и происходит, натуральное преобразование это ведь морфизм между морфизмами

но тогда ^t -> ^f не может быть, потому что тип ^f - bool -> bool, и он не может приниматьаргументом ^t

Ну вообще объект это вещь совершенно необязательная, объекты это просто способ выбрать id-стрелки

Вот у меня как раз какое-то такое интуитивное ощущение появилось

Бартош в своей книжке пишет, что So we can always recover a set monoid from a category monoid. For all intents and purposes they are one and the same.

Ощущение хорошее и правильное, на нём построен формализм категорий в ETCS

я с этим не спорил, я говорил что у фунок кайнд не совпадает

^t -> ^f  стрелка должна иметь тип (bool -> bool) -> bool -> bool

Немного некорректно, да. На моем рисунке стрелки - это не просто ^f и ^t, а ^f* и ^t*

Так, давайте без аналогий

Кайндов в теории категорий нет, и типов тоже

Добрый вечер. Вопрос - а где-нибудь сказано что терминальный объект должен быть населен единственным значением или нет?

а то мне интуитивно казалось что это так, тем более бартош пишет про picking an element когда говорит про морфизм () -> a