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

[deniok]

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

Comments

[sassa-nf.livejournal.com]

"X×Y ≈ Y×X, но знак равенства ставить будет практически неудобно ;-)"

А как мы можем отличить, у кого X слева, а у кого - справа? Как мы даже можем отличить, что у них X с разных сторон? Вроде бы всё, что можно заключить, так это что "это тоже X×Y, хотя и не идентичный объект". Я правильно понимаю, что это просто так визуально на бумаге отображают, а на самом деле X×Y может быть выражено более, чем двумя способами?


"Во-вторых, при чём тут well-pointed'ность?"

Ну я думал, что well-pointedность сводится к тому, что 1 - не инициальный объект. Хотя на самом деле, если смотреть поточечно, то нужно наличие морфизмов из 1 в каждую точку каждого X.

Хом-функторы - это мне ещё предстоит...

[nivanych.livejournal.com]

> X×Y может быть выражено более, чем двумя способами?

Даже X может быть выражено более, чем двумя способами ;-)
Множества из 3 стульев дома и 3 стульев в рабочем кабинете — не равны, но изоморфны! ;-)

[sassa-nf.livejournal.com]

но это же разные 3 стула :)

ок, я думаю, пример понятный, спасибо.

[nivanych.livejournal.com]

Ну или более строгие примеры.
Отрезки натуральных чисел [0,100] и [100,200].
Отрезки вещественных чисел [0,1] и [100,200].