Oℕ
В любом случае, говорить, что у нас в категориях изоморфизм заменяет равенство, неверно.
Вне зависимости от того, можем ли мы определить равенство объектов.
Вне зависимости от того, можем ли мы определить равенство объектов.
эх, хорошо
Size: a a a
2019 October 17
ЕО
Мне кажется, что нельзя определить изоморфизмы, не опираясь на равенство...
V
Видимо, в обычных построениях поверх NBG, это сделать можно.
А так-то, конечно, зависит...
Многочо зависит, про что-то сразу и не скажешь...
А так-то, конечно, зависит...
Многочо зависит, про что-то сразу и не скажешь...
Поэтому неверно говорить, что это верно всегда. Это верно только в теоретико-множественных основаниях теории категорий.
NI
эх, хорошо
Ну вот представь тупл (String, String). А лучше record ;-)
Если ты поменяешь местами, получится изоморфный тип.
И вот теперь представь, что ты в конкретной программе, заменил этот тип на изоморфный ;-)
Если ты поменяешь местами, получится изоморфный тип.
И вот теперь представь, что ты в конкретной программе, заменил этот тип на изоморфный ;-)
NI
Поэтому неверно говорить, что это верно всегда. Это верно только в теоретико-множественных основаниях теории категорий.
В идрисе, кажется, тоже можно за счёт гетерогенности равенства.
NI
Мне кажется, что нельзя определить изоморфизмы, не опираясь на равенство...
Изоморфизмы опираются на равенство "параллельных" стрелок.
V
В идрисе, кажется, тоже можно за счёт гетерогенности равенства.
OK, теоретико-множественно-подобных
NI
OK, теоретико-множественно-подобных
Так идрис ещё никто не обзывал! ;-) ;-)
Да понятно, что уж.
Да понятно, что уж.
NI
эх, хорошо
Вот прямщас, у меня перед глазами, SQL'ные таблички.
И у них много полей одинаковых типов.
Вот бы кто-то их переставил! ;-)
И у них много полей одинаковых типов.
Вот бы кто-то их переставил! ;-)
Oℕ
Ну вот представь тупл (String, String). А лучше record ;-)
Если ты поменяешь местами, получится изоморфный тип.
И вот теперь представь, что ты в конкретной программе, заменил этот тип на изоморфный ;-)
Если ты поменяешь местами, получится изоморфный тип.
И вот теперь представь, что ты в конкретной программе, заменил этот тип на изоморфный ;-)
Если я заменю этот тип на изоморфный, добавив автоматически применение изоморфизма во все конструкции всё будет ок
NI
Если я заменю этот тип на изоморфный, добавив автоматически применение изоморфизма во все конструкции всё будет ок
Речь шла об изоморфизме, как равенстве.
Oℕ
Я понимаю, что моё утверждение неверное, но если его перефразировать как
"Вместо равенства на объектах в качестве отношения эквивалетности расхоже использование изоморфизма"
"Вместо равенства на объектах в качестве отношения эквивалетности расхоже использование изоморфизма"
Oℕ
Будет ок?
NI
Стоит добавить, что в каких-то случаях возможно.
NI
Есть ли вообще понятие образа в категории Set?
Такое понятие есть в так называемых регулярных категориях.
Set — регулярная, как и любой топос и претопос.
Одно из возможных определений регулярных категорий —
A regular category is a finitely complete category with pullback-stable image factorizations.
https://ncatlab.org/nlab/show/regular+category
https://en.wikipedia.org/wiki/Regular_category
Set — регулярная, как и любой топос и претопос.
Одно из возможных определений регулярных категорий —
A regular category is a finitely complete category with pullback-stable image factorizations.
https://ncatlab.org/nlab/show/regular+category
https://en.wikipedia.org/wiki/Regular_category
NI
"Image factorizations", это как раз и есть разделение стрелки на две — epi и mono.
В каких-то категориях, факторизации могут быть и другие.
Само понятие интересное, оно ведёт к понятию модельных структур.
Внутренняя логика регулярных категорий, ВНЕЗАПНО, называется регулярной. Интересная штука, что-то навроде самого минимума, вокруг которого можно строить датабазу. С пролого-подобным тоже так же связано.
В каких-то категориях, факторизации могут быть и другие.
Само понятие интересное, оно ведёт к понятию модельных структур.
Внутренняя логика регулярных категорий, ВНЕЗАПНО, называется регулярной. Интересная штука, что-то навроде самого минимума, вокруг которого можно строить датабазу. С пролого-подобным тоже так же связано.
AK
@Comonoid, @odomontois, спасибо!
2019 October 22
Oℕ
can someone explain what homotopy type theory is/the problems the field is interested in/its goals and how this relates to category theory and type theory?
AG
хотт-тюториалы будут монадными тюториалами 20х