Oℕ
тогда почему не n!m!k!?
Потому что не обязательно при построении изоморфизма между парами пользоваться только изоморфизмами между отдельными компонентами
Size: a a a
2020 February 28
A
Oℕ
тогда почему не n!m!k!?
Например сколько есть изоморфизмов (Bool, Bool) -> (Bool, Bool)
A
да, я понял. (n*m*k)!
Oℕ
Ну в общем ответ: много.
И это мы о конечных типах говорим.
Представьте что в случае бесконечных.
И это мы о конечных типах говорим.
Представьте что в случае бесконечных.
A
ну ... обычно когда говорят об изоморфизме, то там еще какую-то структуру надо сохранить, а это сразу очень ограничивает
Oℕ
Как мы уже говорили, у объектов мы не требуем наличие структуры
Oℕ
Мы лишь демонстрируем, что для некоторых категорий изоморфизмы между произведениями часто случаются неуникальными
Oℕ
На примере обожаемой вашей категории
G
У меня другое число получилось
Тогда странно, что алгебра типов использует именно такую нотацию. Я понимаю, что + и * на типах - это не одно и то же, что и мощности множеств, но всё равно
Oℕ
Тогда странно, что алгебра типов использует именно такую нотацию. Я понимаю, что + и * на типах - это не одно и то же, что и мощности множеств, но всё равно
одно и то же
Oℕ
у вас ((A, B) , C)
Oℕ
((A x B) x C)
G
А, я проглядел
Oℕ
откуда сумма взялась
G
Подумал, что там тип-сумма
G
G
Спать побольше надо
G
Количество чего это
Количество всех перестановок множества
G
После этого возьмите три разных натуральных числа m, n и k
Сколько элементов содержит
((Fin n, Fin m), Fin k) ?
Сколько элементов содержит
((Fin n, Fin m), Fin k) ?
n * m * k?