к
То есть нужно в iso добавить два равенства?
Size: a a a
2018 April 06
KV
То есть нужно в iso добавить два равенства?
Да
AG
да f.g = id + g.f = id
Oℕ
Можно в имеющемся коде добавить равенства и будет доказательство. Оно, конечно, не общее, а для частного случая, но с общим совпадает по виду
Да. Тут на самом деле дл таких простых штук не нужно хотт воротить. Доказать можно даже с в общем случае даже на каком-нибудь пурскрипте
KV
Да. Тут на самом деле дл таких простых штук не нужно хотт воротить. Доказать можно даже с в общем случае даже на каком-нибудь пурскрипте
На пурскрипте??? Жесть какая, я себе этого не могу представить
AG
на самом деле нет, там почти сразу экстенсиональность вылазит
Oℕ
на самом деле нет, там почти сразу экстенсиональность вылазит
Да не нужна она там
к
Может кто написать пример на коке правильного доказательства этого просто примера, чтобы потом использовать за основу?
AG
ну для рефла-транса не нужна конещ
к
На идрисе сложно, мне бы на коке)
к
Но спасибо
KV
На идрисе сложно, мне бы на коке)
https://github.com/jwiegley/category-theory/blob/master/Theory/Isomorphism.v
Вроде бы вот, но тут не всё так просто
Вроде бы вот, но тут не всё так просто
NI
Ох, во что программисты тёплый ламповый категорный чатег превратили ;-)
KV
Короче, для честного доказательства нужно определять категории, а это уже порождает некоторую сложность
к
Ох, во что программисты тёплый ламповый категорный чатег превратили ;-)
Ну не на бумаге же доказывать
к
Это слишком сложно
KV
Это слишком сложно
Ха-ха
KV
Объяснить что-то самому себе проще, чем компьютеру. Это касается нетривиальных вещей, а с тривиальными наоборот