Oℕ
Для них получается нужно явно потребовать малость Ob
Size: a a a
2020 April 19
DK
Ты про "протоморфизмы" из динозавров?
Oℕ
Ты про "протоморфизмы" из динозавров?
нет
Oℕ
Второе опредедение https://ncatlab.org/nlab/show/category здесь, например
к
хм по этому определению, если композиция это функция, а функция по ссылке это гомоморфизм множеств, то коллекция объектов - множество)
DK
Какой учебник лучше использовать?
к
Второе опредедение https://ncatlab.org/nlab/show/category здесь, например
не понимаю
если по этому определению потом определить, что
Mor(C) := U(x, y in Ob(C)), C_1(x, y)
если Mor(C) множество, то разве это не значит, что его подмножества - тоже множества? Если мы берем подмножество единичных, то это подмнжество - множество, а оно биективно коллекции объектов, получается коллекция объектов тоже множество
то есть isSet(Mor(C)) -> isSet(Ob(C)) выполняется даже для этого определения
если по этому определению потом определить, что
Mor(C) := U(x, y in Ob(C)), C_1(x, y)
если Mor(C) множество, то разве это не значит, что его подмножества - тоже множества? Если мы берем подмножество единичных, то это подмнжество - множество, а оно биективно коллекции объектов, получается коллекция объектов тоже множество
то есть isSet(Mor(C)) -> isSet(Ob(C)) выполняется даже для этого определения
к
к чему эти рассуждения про пересечения мне тоже не понятно, возможно я что-то упускаю важное в самом начале и вопрос в другом вообще
A
проблема в том, что может биекции не получится
A
если один и тот же морфизм будет единичным для нескольких объектов
A
но это немного абсурдно
A
то, что так не бывает, и выражается в том, что хомсеты дизъюнкты
к
да, действительно, хороший пример, я в таком случае предполагал, что это один и тот объект, мол объекты стягиваются в один, но в определении ничего подобного нет конечно
для этого достаточно более слабого ограничения, что forall a b, a /= b <-> ida /= idb, ну или прямо затребовать биекцию и отказаться от объектов
для этого достаточно более слабого ограничения, что forall a b, a /= b <-> ida /= idb, ну или прямо затребовать биекцию и отказаться от объектов
2020 April 22
к
что-то мне такое соглашение не ясно, если взять p = hom, то hom(a, b) это будет b -> a, то есть тут очевидно это некое соглашение не выполняется
так вот, я хотел узнать, это локальное соглашение для статьи, или реальное соглашение при интерпретации профункторов как отношений?
так вот, я хотел узнать, это локальное соглашение для статьи, или реальное соглашение при интерпретации профункторов как отношений?
к
Oℕ
Ну над любым множеством можно провести трункацию в один элемент.
Грубо говоря отношение P(x, c) существует, когда множество P(x, c) непусто
Грубо говоря отношение P(x, c) существует, когда множество P(x, c) непусто
Oℕ
Такое сведение множеств к отношениям\свойствам\утверждениям встречается нередко
Oℕ
В каком-то смысле вся идея proposition as types держится на этом подходе
к
не-не, я про конкретно отношение в самом начале абзаца: P x c is interpreted as a relation c P x
к
ну про то что порядок аргументов поменялся