для одной из них те же проблемы должны возникнть

в лине есть функц. экстенсиональность нормальным способом?

не знаю что значит нормальным способом, но каким-то способом есть

встроена аксиома
propext : ∀ {a b : Prop}, (a ↔ b) → a = b

из которой каким-то образом следует funext

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

quot.sound : ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b

)

Что-то я задумался.
А почему не может быть  "g . f = id_a, h . f = id_a", но при этом "g != h"?
Какая из аксиом или определений категории это запрещает?

ну вот непрямой путь доказать

пусть f : A -> B - изоморфизм, обратный морфизм - g : B -> A
f.g = id_B
g.f = id_A

докажем, что для любого f, если существуют g1 и g2 такие, что (f, g1) и (f, g2) - изоморфизмы, то g1 = g2

так как (f, g1) и (f, g2) - изоморфизмы, то
f.g1 = id_B
f.g2 = id_B
следовательно
f.g1 = f.g2

так как f - мономорфизм (любой изоморфизм - мономорфизм), то
g1=g2

f.g1 = id_B
f.g2 = id_B
значит
f.g1 = f.g2

А вот этот переход почему верен?

транзитивность + симметричность равенства

А они в ТК вводятся?

это равенство не из тк, а из метаязыка для тк

А где Вы видали равенство, которое не симметричное или не транзитивное?

Ну, вроде очевидно, что из того, что я такого не видел не следует, что такого нет :)


Если без шуток, то я ТК очень плохо знаю, только в рамках книги Бартоша. И когда ТК по этой книге изучал, то многие вещи воспринимал "на веру" на интуитивном уровне.

А сейчас у меня вторая попытка поизучать ТК, только более строго. И я в самом начале понял, что даже тривиальные вещи, которые мне казались очевидными, я не могу доказать. Поэтому решил задать такой глупый уточняющий вопрос.

Но я понимаю, что задавать десятки глупых и банальных вопросов в чате — это не правильный путь. А правильный попробовать, всё-таки, вникнуть в то, что написано у Маклейна (или в другой книге со "строгими доказательствами").

Добавлю ещё: Basic Category Theory (Tom Leinster) и http://cadadr.org/notes/categories.pdf

> Ну, вроде очевидно, что из того, что я такого не видел не следует, что такого нет :)
Это следует из других соображений, но ладно

Это не недоказуемость, а negation as failure

А никто не встречал какого-нибудь визуализатора для ТК?
Чтобы поддерживал вещи вроде: ты ему задаёшь две категории, а он тебе рисует их произведение.

@stask что-то такое делал

лучше поискать такие инструменты для графов я думаю

Согласен, что тоже выход.
Но специализированные для ТК могут иметь полезные доп. фичи.

В любом случае, если кто-то что-то похожее (хотя бы отдалённо) видел — буду благодарен за инфу.

а как в принципе предполагается нарисовать "категорию"