Oℕ
То есть dom и cod будут «возвращать» id, я верно понял? И эти id будут заменять нам объекты из привычного мне определения категории?
Да
Size: a a a
2020 July 27
AK
Тогда второй вопрос про =. В определении нет какого-то описания что такое =. Мы ожидаем от него рефлексивность, транзитивность и симметричность?
Oℕ
Это определение примерно обобщается до "внутренней категории", но там объект объектов и объект морфизмов снова два разных объекта, а "подмножество" - это морфизм id: O -> H
AK
Затык появляется, когда я пытаюсь в качестве класса взять не множество, а тип
Oℕ
Тогда второй вопрос про =. В определении нет какого-то описания что такое =. Мы ожидаем от него рефлексивность, транзитивность и симметричность?
Это вообще сложный вопрос, у категорий могут быть разные основания, это оставляется для откуп метатеории.
Лучше об этом расскажут @valery_isaev и @Comonoid
Лучше об этом расскажут @valery_isaev и @Comonoid
Oℕ
Затык появляется, когда я пытаюсь в качестве класса взять не множество, а тип
и какой затык
AK
Не могу сравнить
AK
Пробовал в coq
Oℕ
Не могу сравнить
что значит "сравнить"
AK
Не могу доказать ассоциативность композиции. Они синтаксически не равны
Oℕ
В coq например у вас есть встроенный тип =, его элементы например можно считать равенстваии
Oℕ
Не могу доказать ассоциативность композиции. Они синтаксически не равны
Композиции в Set?
Oℕ
Вы можете ввести аксиому functional extensionality,
Oℕ
И доказывать с её помощью
IJ
Во-первых, вы уверены что это про теоркат? Во-вторых, в coq просто введите отдельное отношение для экчтенсионального равенства между функциями
IJ
Не =
AK
Пробовал определить тайпкласс параметризованный типом объектов. Ещё не дочитался до functional existentionality. Буду рыть в эту сторону, спасибо!
AG
равенство в пруверах и вообще логике это сложная тема, последние достижения на этой почве привели к гомотопическим теориям типов
AK
Во-первых, вы уверены что это про теоркат? Во-вторых, в coq просто введите отдельное отношение для экчтенсионального равенства между функциями
Как новичку в теоркате мне не понятно понятие равенства в определении
Oℕ
Во-первых, вы уверены что это про теоркат? Во-вторых, в coq просто введите отдельное отношение для экчтенсионального равенства между функциями
Ну человек явно ещё не готов к сетоидам. В идрисовской формулировке они там именно, что пользуются встроенным равенством и просто аксиомы направо и налево лепят