Oℕ
они все каких-то квошентов требуют
Size: a a a
2020 July 27
Oℕ
все, что сложнее списков
NI
Это вообще сложный вопрос, у категорий могут быть разные основания, это оставляется для откуп метатеории.
Лучше об этом расскажут @valery_isaev и @Comonoid
Лучше об этом расскажут @valery_isaev и @Comonoid
Так что тут рассказывать...
Для разных оснований получаем несколько разные теории категорий с несколько разными свойствами.
Для разных оснований получаем несколько разные теории категорий с несколько разными свойствами.
NI
Это в смысле чтобы определение категории сразу с равенствами писать?
А как ещё категорию сделать без равенств?
Сразу при "создании" категории, они каким-то образом должны быть определены.
Сразу при "создании" категории, они каким-то образом должны быть определены.
KV
А как ещё категорию сделать без равенств?
Сразу при "создании" категории, они каким-то образом должны быть определены.
Сразу при "создании" категории, они каким-то образом должны быть определены.
Это я имел в виду, что не как обычно, делать рекорд и в него равенства пихать, а построить тип, содержащий категорный синтаксис, который потом будет интерпретироваться в конкретных категориях. Ну и в этот тип конструкторы-равенства добавить, чтобы их сохранение проверялось
NI
Это я имел в виду, что не как обычно, делать рекорд и в него равенства пихать, а построить тип, содержащий категорный синтаксис, который потом будет интерпретироваться в конкретных категориях. Ну и в этот тип конструкторы-равенства добавить, чтобы их сохранение проверялось
Очень много тут нюансов попутно возникает... ;-)
ЕО
Тогда второй вопрос про =. В определении нет какого-то описания что такое =. Мы ожидаем от него рефлексивность, транзитивность и симметричность?
Равенство это зло :) Вообще теоркат строят поверх теории множеств или теории классов, и юзают их равенство. Подозреваю, что вы доказываете что-то, что недоказуемо в интииционистской математике
NI
> Равенство это зло :)
Дадад. Неизбежное зло, причём ;-)
Дадад. Неизбежное зло, причём ;-)
χλ
> Равенство это зло :)
Дадад. Неизбежное зло, причём ;-)
Дадад. Неизбежное зло, причём ;-)
Но можно же какие-то утверждения делать без равенств?
χλ
Пробовал ли кто-то содержательные системы без равенства строить?
NI
Но можно же какие-то утверждения делать без равенств?
Да можно, конечно.
Просто слишком много, где оно так и так нужно.
Просто слишком много, где оно так и так нужно.
NI
Пробовал ли кто-то содержательные системы без равенства строить?
Надо уточнять, что такое "без равенства".
χλ
Надо уточнять, что такое "без равенства".
Пожалуй надо
Но как корректно уточнить?
Но как корректно уточнить?
ЕО
> Равенство это зло :)
Дадад. Неизбежное зло, причём ;-)
Дадад. Неизбежное зло, причём ;-)
Ну всё-таки в интенсиональной теории типов настоящих равенств нет, есть отношения эквивалетности
2020 July 28
NI
Ну всё-таки в интенсиональной теории типов настоящих равенств нет, есть отношения эквивалетности
Тогда это ответ на вопрос выше ;-)
2020 July 29
ЕО
Тогда это ответ на вопрос выше ;-)
Можно даже без отношений эквивалентности, но с порядками (правилами редукции, например) жить. Конечно в классической математике по правилам редукции можно отношение эквивалентности построить, но в интуиционизме не всегда.
2020 August 01
SK
Расскажите, что за анти-спам бота вы используете?
2020 August 02
AZ
А есть какое-то обобщающее название для всяких monadic-like операций? Например, есть обычная монада, а есть например линейная. Она чуть другая и в тот же тайпкласс Monad не лезет, но по сути что-то очень похожее
χλ
А есть какое-то обобщающее название для всяких monadic-like операций? Например, есть обычная монада, а есть например линейная. Она чуть другая и в тот же тайпкласс Monad не лезет, но по сути что-то очень похожее
Но это же к теории категорий отношения не имеет...
AZ
почему? Монада из категорий же, линейная тоже должна иметь какое-то отображение