V
Получается, т.к. мы сконструировали только один объект, и никакого единичного объекта нет, внутрь него мы пока залезть не можем.
Что значит единичного объекта нет? Есть.
Size: a a a
2018 November 02
V
Или я чего-то не понял
V
Мы просто сконструировали конкретный объект в категории пространств/типов.
V
Но остальные же типы никто не отбирал)
V
И что значит "залезть внутрь" вообще не понятно
Oℕ
А т.е это тип, у нас остаётся терминальный тип
V
А т.е это тип, у нас остаётся терминальный тип
Ну да
Oℕ
Но новый тип, скажем так, не снабжён конструкторами из этого построения
V
Как не снабжен? У него есть одна точка.
Oℕ
Аааааааа
V
Пути -- это тоже конструкторы, только высшие. А 0-конструктор один всего, да.
Oℕ
Это тип с одним нулларным конструктором, и пачкой равенств и равенств над равенствами
V
Ага
V
Только не 0-арным, а нульмерным)
Oℕ
А арность - это про что? Про что-то типа гомотипического уровня?
V
Арность -- число аргументов функции)
Oℕ
А ну да, он одноместный из единицы
V
Гомотопический уровень -- это как раз (раз)мерность
Oℕ
Но разве это не то же самое, что нуль местный?
V
Но разве это не то же самое, что нуль местный?
То же самое, но я сказал меРный, а не меСТный