P
он это назвал так, хотя упомянул, что название не официальное, но другого я не знаю
Size: a a a
2021 May 04
P
потому что это завязано на построение логики второго порядка?
P
и я так понимаю, что можно вообще без аксиоматик ТМ обойтись, если через ТТ строить или нет? у меня просто пока в голове эти вещи никак не слипнутся: ТК, ТМ и ТТ
ЕО
Можно, конечно, без аксиоматик ТМ обойтись, но всё равно полноценная ТК содержит Set, а значит автоматически содержит выделенную модель ТМ.
P
это да, но уже как частный случай строится
ЕО
На практике ТК это просто один из способов аксиоматизаций множеств (и классов)
P
просто меня смутило, что они не эквивалентные, эти определения
ЕО
Просто "размеры" отличаются, вот и определения неэквивалентны.
NI
Ещё и надо различать, на основе какой логики эти построения сделаны.
NI
Щас полностью проработаны только классические предикаты первого порядка.
Немного прорабатывать пробовать интуиционизм.
Наверное, гомотопическое тут стоит поставить отдельно, тоже прорабатывают, см. те же категрии в Аренд.
А вот полностью на линейной логике, кажется, пока никто не пытался ;-)
Немного прорабатывать пробовать интуиционизм.
Наверное, гомотопическое тут стоит поставить отдельно, тоже прорабатывают, см. те же категрии в Аренд.
А вот полностью на линейной логике, кажется, пока никто не пытался ;-)
P
разве логика в HoTT — не интуиционистская модель?
ЕО
На линейной логике это как? Нужно декартово произведение, чтобы internal категорию определить
V
Это определение, которое "map theory", какое-то странное, оно действительно неэквивалентно обычному определению категорий, и это никак не связано с размерами или чем-то таким, вообще не понятно зачем его использовать. Возможно это какой-то устаревший вариант. Вообще, в Categories, Allegories много таких необщепринятых определений.
NI
Стоит отличать её от обычного интуиционизма.
P
ага, понял, спасибо
NI
Ну будут другие конструкции, что уж тут.
То же и с интуиционизмом - например, без аксиомы выбора возникают проблемы с определеним эквивалентности категорий.
То же и с интуиционизмом - например, без аксиомы выбора возникают проблемы с определеним эквивалентности категорий.
2021 May 17
Oℕ
@white_bear0 тут можно даже в поиске найти, тема поднималась несколько раз
2021 May 19
ЕО
Товарищи, давайте без стикеров
a
их можно заблокать в настройках
ЕО
Ну, пойдём на тоталитарные меры, если не подействует слово