МБ
Тайпчекер не покажет ошибку. Просто позволит доказать h = g.
Size: a a a
2021 June 27
DG
Понял, спасибо!
KV
Хотя нет, чего это я. Легко бы доказалось, при любой формализации
к
как-то так выглядит описание категории без
hк
при добавлении h мы получаем недоказуемую цель. Ну вот и все. В голове до этого равенство (h . f = g . f = id_a) не вызывало конфликтов
Но именно в этом случае получается что f это изоморфизм, а у конкретного изоморфизма есть только один обратный элемент
Но именно в этом случае получается что f это изоморфизм, а у конкретного изоморфизма есть только один обратный элемент
KV
У меня в голове было равенство
g . f . h = g . f . h
g . f . h = g . f . h
к
да, это оно есть (до симплификации)
g . (f . h) = (g . f) . h
[ f . h = id_b, g . f = id_a ]
g . id_b = id_a . h
g = h
ассицативность не доказывается
g . (f . h) = (g . f) . h
[ f . h = id_b, g . f = id_a ]
g . id_b = id_a . h
g = h
ассицативность не доказывается
Oℕ
это, правда, не является решением задачи на лине
Oℕ
скорее является нерешением обратной задачи
KV
Наверное потребуется некоторое лишнее усилие, чтобы показать, что g . f = id, h . g = id, и наоборот
Ну а так не вижу проблем
Ну а так не вижу проблем
к
а, ну да, ошибся, имел в виду в целом формализация категорий не на бумажке, а где-то, кто тебя проверит
Oℕ
а в лине разве встроено не то же самое проблемное равенство, которое довольно сомнительным делает формализацию тк на коке, идрисе и т.п.
к
у меня не было никакого опыта доказательств, кроме геометрии в школе, поэтому очень сложно понять, что такое доказательство на бумажке и как их делать, и когда я это делаю в какой-нибудь книге, то каждый раз чувствую, что где-то я сделал что-то не то, но проверить некому, в книжках нет ответов с доказательствами
так можно хотя бы часть неуверенности убрать
так можно хотя бы часть неуверенности убрать
к
скорее всего то же. А что именно это за свойство равенства, которое делает сомнительным формализацию?
МБ
Недоказуемость, в общем-то, ничего не означает, насколько я всю эту конструктивную философию понимаю. Вдруг, просто не удалось построить доказательство, а оно есть какое-то.
к
ну, это просто будет не решением задачи в лине, но это позволит уже решить ее на бумжке
Oℕ
а вы доказывали ассоциативность функторов?
к
эта формализация нам показывает, что h.f = id_a - невалидная категория
на бумажке уже можем показать, что других кандидатов на композицию нет, значит категорий и нет
на бумажке уже можем показать, что других кандидатов на композицию нет, значит категорий и нет
к
доказывал ассоциативность естественных преобразований, но функторов кажется нет
Oℕ
для какой композиции?