EJ
Универсальный конус над пустой диаграммой - терминальный объект.
Size: a a a
2021 April 11
EJ
Для конкретных категорий существование экспонент - это возможность каррирования: возможность функцию нескольких переменных свести к набору функций от одного переменного. Для функции двух переменных это означает, что фиксирование любого возможного первого аргумента даёт функцию от второго аргумента.
EJ
Классификатор подобъектов - такой специальный объект O, что для любого объекта X подобъекты этого X в точности соответствуют морфизмам из X в O.
S
Хмм, а откуда эти картинки ?
ЕО
Проще сказать, что замкнуты все конечные диаграммы. Конечно достаточно лишь существование лишь расслоенных произведений, но с конечными диаграммами проще
EJ
Просто нарисованы в редакторе.
S
Жесть кароче. Ничего не понял. А как это относится к хоту, можно понять?
P
разве это достаточное условие? важно же, чтобы объекты над которыми строят конус образовывали подкатегорию тоже, нет?
Oℕ
Я могу попробовать свою интуицию объяснить, если вам интересно
P
объясни, мне интересно
P
я так понимаю, там карирование функциональных типов задается похожим образом, да?
Oℕ
ну мне кажется начилие конечных лимитов и замкнутость не самые интересные качества, кажется, что самый тонкий момент в топосе - это subobject classifier
Oℕ
Т.е. первые два позволяют строить объекты с требованиями каких-то "свойств"
Ну например, имея объект A, мы можем получить множество "бинарных морфизмов" (A x A => A)
Далее, стартуя с какого-то утроенного объекта и бинарного морфизма мы можем получить, ну например правоассоциированную композицию трёх элементов
fr: (A x A x A) x (A x A) => A) -> A
fr = apply . <<pi1 . pi1, apply. pi2. assoc>>
Ну например, имея объект A, мы можем получить множество "бинарных морфизмов" (A x A => A)
Далее, стартуя с какого-то утроенного объекта и бинарного морфизма мы можем получить, ну например правоассоциированную композицию трёх элементов
fr: (A x A x A) x (A x A) => A) -> A
fr = apply . <<pi1 . pi1, apply. pi2. assoc>>
Oℕ
что примерно будет соответствовать "фп" коду
fr( (x, y, z) , f) = f(x, f(y, z))
fr( (x, y, z) , f) = f(x, f(y, z))
Oℕ
примерно так же можем получить левоассоциированную
fl : (A x A x A) x (A x A) => A -> A
fl = apply . < <pi2, apply . <<pi1.pi1 . pi1, pi2. pi1. pi1>, pi2> , pi2>
fl((x, y, z), f) = f((x, y), z)
fl : (A x A x A) x (A x A) => A -> A
fl = apply . < <pi2, apply . <<pi1.pi1 . pi1, pi2. pi1. pi1>, pi2> , pi2>
fl((x, y, z), f) = f((x, y), z)
Oℕ
тут скорее всего куча неточностей, но идея, понятна
Oℕ
оба таких морфизма мы можем каррировать относительно первого аргумента, получив два морфизма
((A x A) => A) -> (A x A x A) => A
и найдя их эквалайзер получить не просто бинарные функции, а ассоциативные бинарные функции
((A x A) => A) -> (A x A x A) => A
и найдя их эквалайзер получить не просто бинарные функции, а ассоциативные бинарные функции
Oℕ
но дальше самое интересное, из этого эквалайзера, очевидно существует мономорфизм включения обратно во все бинарные морфизмы
Oℕ
таким образом мы задаём свойство "ассоциативности" для наших бинарных морфизмов, и вот вопрос - какой механизм рассуждения о "свойствах" предлагает наш топос
Oℕ
википедия говорит, что каждый мономорфизм должен быть эквивалентен какому-то пулбеку в такой форме