От теории множеств к теории типов

[deniok]

От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо alexey_rom за ссылку.

Comments

[nivanych.livejournal.com]

Из записи XxY не следует какое-то представление индексов, а только то, что их два штук.
Несколько образно, индексами мы обозначаем места, куда можно что-то "положить".
Так вот, если есть два индекса x и y, то мы на место x можем "положить" Y, а можем и X, например.

Декартово произведение задаёт с собой сразу и проекции. Это хорошее такое произведение.
Но не каждое моноидальное произведение позволяет потом "раздербанить" произведение по составляющим.

[sassa-nf.livejournal.com]

"Из записи XxY не следует какое-то представление индексов, а только то, что их два штук."

да, я это понимаю. я пытаюсь понять, "направленность" у X×Y "глобально видима" или как? То есть, "какое-то представление индексов" понятно.

Я оба произведения понимаю, и понимаю, почему изоморфны. Я не знаю наверняка, существенно ли, что Y×X пишется в обратном порядке. Это просто запись такая, чтобы не выглядело тавтологично "X×Y ≈ X×Y"? Или есть способ выделить "направленность" и для каких-то двух объектов можно выяснить, что они одинаковой "направленности"?

(ну, я не знаю - может, где-то в какой-то книжке написано, а я читал не то? из того, что я читал, никак не следует, что можно выяснить "направленность" двух разных произведений)

[nivanych.livejournal.com]

> выяснить "направленность"

Исходя из каких данных выяснить?
Произведение уже направлено по определению — есть две различимых проекции, составляется произведение тоже вполне так "направленно".
Принято в n-арном произведении всякое умножаемое писать упорядоченной цепочкой типа XxYxZxTxUxV или (X,Y,Z,T,U,V). И то, что отдаст первая проекция, принято писать слева. Соответственно, отличать XxY от YxX, если как-то отличаем X и Y.
Тем не менее, в категорном, достаточно часто выписывают проекции явно, тем самым, устраняя ещё одну возможность неоднозначности понимания. И это хорошо, как правило.

[sassa-nf.livejournal.com]

Я не знаю, как уточнить свой вопрос. Пока что понятно не стало.

"Исходя из каких данных выяснить?"

ага, это мой вопрос.


"Произведение уже направлено по определению"

блин, ну, как же направлено, если проекции индексируются сетоидом I. Я понимаю, что можно записать сетоид в виде списка. Я понимаю, что сетоида достаточно, чтобы знать, как применить проекцию.

давайте попробую ещё раз по частям.

∏{X}_{i,j} и ∏{X}_{i,k}

1. это произведения одного и того же X_i и разных X_j, X_k? или в каждом случае i - просто индекс, а потому X_i первого не обязательно X_i второго? Типа как в арифметике запись ΣX_i i не означает ничего, кроме способа выбрать X_i в этой одной сумме, и не означает, что в двух разных записях X_i references одно и то же значение.

2. если X_i в обоих записях означает один и тот же X_i, то что задаёт порядок i в сетоиде, ...кроме договорённости записывать i, j, k в алфавитном порядке.

3. Я сейчас считаю, что ∏{X}_{i,j} эквивалентно записи X_i×X_j и эквивалентно записи X_j×X_i, поскольку порядок i, j отсутствует. Откуда тогда следует направленность произведения?

[nivanych.livejournal.com]

> проекции индексируются сетоидом I.

Строго говоря, классические проекции индексируются дискретной категорией (в которой стрелки только единичные).
И произведение, это предел некоторого функтора из этой категории.
Какие претензии к этом определению? ;-)

А касаемо вопросов — это должно быть всегда ясно из контекста.
Если не ясно, значит херово написали.