В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Теория категорий

623 membersпожаловаться на группу
2021 June 15

NI

Nick Ivanych in Теория категорий
Для топосов есть внутренний язык, который выражает всё, что внутри них происходит.
Так называемый Mitchell-Benabou language -
https://ncatlab.org/nlab/show/Mitchell-B%C3%A9nabou+language
источник
21:40пожаловаться#1

AG

Alex Gryzlov in Теория категорий
с топосами насколько я знаю, есть проблема в плане того что это слишком сильная конструкция
источник
22:51пожаловаться#2

NI

Nick Ivanych in Теория категорий
В некотором смысле, да.
Что не всё полезное дотягивает до топоса.
источник
22:51пожаловаться#3

ЕО

Евгений Омельченко... in Теория категорий
Т.е. у них нет вычислимой модели?
источник
22:51пожаловаться#4

AG

Alex Gryzlov in Теория категорий
там сразу вываливается propositional extensionality, импредикативность, каноничность как правило ломается
источник
22:52пожаловаться#5

ЕО

Евгений Омельченко... in Теория категорий
А что такое "каноничность"?
источник
22:52пожаловаться#6

AG

Alex Gryzlov in Теория категорий
любой замкнутый терм редуцируется до нормальной формы
источник
22:53пожаловаться#7

V

Valery in Теория категорий
какие есть модели, которые не поддерживают эти свойства?
источник
22:54пожаловаться#8

ЕО

Евгений Омельченко... in Теория категорий
Обычно привык к тому, что это называют тотальностью. Но вообще интересно, умозрительно не кажется ведь, что топосы настолько сложные. По сути это ведь MLTT с классификатором подобъектов.
источник
22:56пожаловаться#9

AG

Alex Gryzlov in Теория категорий
так наоборот, насколько я понимаю, от первых двух свойств избавиться сложно, а третье надо каждый раз доказывать
источник
23:13пожаловаться#10

AG

Alex Gryzlov in Теория категорий
ну типа https://ncatlab.org/nlab/show/canonical+form
источник
23:14пожаловаться#11

V

Valery in Теория категорий
Я не понял, что значит "избавиться от первых двух". Утверждение было, что мы не хотим предполагать эти правила по какой-то причине, но по какой? Видимо должны быть какие-то модели, где они не верны, но я таких не знаю (ну кроме синтаксических).
источник
23:16пожаловаться#12

AG

Alex Gryzlov in Теория категорий
я думал, синтаксические модели это как раз идеал :) но я правда этого набрался у французов :)
источник
23:17пожаловаться#13

V

Valery in Теория категорий
Идеал — это Set, всё остальное жалкая имитация :)
источник
23:21пожаловаться#14

ЕО

Евгений Омельченко... in Теория категорий
А какой Set: с аксиомой выбора или без? :)
источник
23:23пожаловаться#15

V

Valery in Теория категорий
ну это уже зависит от философских предпочтений
источник
23:23пожаловаться#16

ЕО

Евгений Омельченко... in Теория категорий
Идеал это Nat, всё остальное -- костыли для изучения свойств натуральных чисел
источник
23:24пожаловаться#17

ЕО

Евгений Омельченко... in Теория категорий
Мы их не хотим предполагать потому, что хочется бесплатно получить пруф ассистент, как мне кажется
источник
23:28пожаловаться#18

AG

Alex Gryzlov in Теория категорий
ну да, синтаксические модели для того и строятся, как я понимаю
источник
23:29пожаловаться#19

AG

Alex Gryzlov in Теория категорий
французы сравнивают семантические модели с интерпретаторами, а синтаксические с компиляторами
источник
23:31пожаловаться#20