История изменений
Исправление quasimoto, (текущая версия) :
ЭТо язык логики первого порядка
«Понятие топоса представляет в объективной категорной форме сущность логики высшего порядка» (с) Ловер. Внутренний язык элементарного топоса без ограничений это многосортная интуитивистская логика высшего порядка (которая превращается в классическую при допущениях). Это в случае 1-топосов. А HoTT вообще изучает внутренние языки (\inf, 1)-топосов, то есть n-категорное обобщение.
Ну и да — а какой толк? А какой толк от таблицы Менделеева?
Исходная версия quasimoto, :
ЭТо язык логики первого порядка
«Понятие топоса представляет в объективной категорной форме сущность логики высшего порядка» (с) Ловер. Внутренний язык элементарного топоса без ограничений это многосортная интуитивистская логика высшего порядка (которая превращается в классическую при допущениях). Это в случае 1-топосов. А HoTT вообще изучает внутренние языки (\inf, 1)-топосов, то есть n-категорное обобщение.