Про равенство функций g,h : B -> Set можно думать как про функцию, сопоставляющую каждому элементу b : B биекцию между g(b) и h(b). Тогда эпиморфность говорит, что если у нас есть биекция между g(f(a)) и h(f(a)) для всех a : A, то у нас есть и биекция между g(b) и h(b) для всех b : B. Теперь вместо Set берем Prop (я написал Set только для иллюстрации мысли), а вместо g и h берем нужные функции, такие, что биекция между g(f(a)) и h(f(a)) строится легко, а биекция между g(b) и h(b) будет давать прообраз b. Конкретно, в качестве g(b) мы берем одноэлементное множество, а в качестве h(b) множество прообразов b (почти).

Вот ещё не очень ясный момент. Получается, что в h(b) доказательство наличия прообраза, но оно равно тому элементу одноэлементного множества, т. е. тривиальной истине. Но из тривиальной истины бы мы не смогли получить прообраз, так? А из h(b) получаем, хотя они равны

Не элементы равны, а сами множества, где под равенством множеств я подразумеваю биекцию между ними. Т.е. g(b) = h(b) означает, что у нас есть биекция {*} = { a : A | f(a) = b }. Ну а из такой биекции легко получить прообраз b.

Я написал "почти" потому что на самом деле такой биекции быть, конечно, не может, т.к. прообразов может быть больше одного.

Поэтому у нас Prop вместо Set, и вместо биекций между множествами "биекции" между утверждениями.

Но _внешне_, когда мы смотрим на эти доказательства, эти две ситуации не отличаются.

Ок, теперь вроде всё ясно. Спасибо!

Досмотрел лекции до функторов, там используют пример Maybe. А List это функтор? Для всех существующих элементов вроде все законы выполняются, но List так же создаёт новые элементы , которых в категории до него просто не было

Это функтор, и он ничего нового не создаёт

Чему соответствует лист из двух элементов в категории без листа?

Произведению объекта самого на себя

Список из произвольного количества элементов соответствует свободному моноиду

А, в List все элементы одного типа только? Да тогда не создаёт, понял

Гетерогенные списки известной финитной длины (тюплы) и типов соответствуют произведению.
Гетерогенный список произвольной длины и набора объектов можно выразить через сумму таких произведений

Бывают функторы с большим чем 1 числом аргументов? Скажем Either - функтор?

Функторы с большим числом аргументов (Би, Три, Про) - это функторы из декартова произведения категорий

Если в категориии С существуют все суммы двух элементов, можно определить бифунктор • + •  : (C x C) -> C

Извините, а какие лекции вы смотрите? В pinned message только тексты вроде, видео-лекций нет. Наверное пропустила, но долистать не могу. Спасибо!

У него три плейлиста по ТК, вот его канал https://m.youtube.com/user/DrBartosz

Класс, спасибо!