TN
если J добавить и Fix то все можно практически сразу
Size: a a a
2017 November 23
TN
а писать программы, которые моделируют (кодируют, пусть и в других языках) нам никто не запрещает, по сути все категорные кодировки — это как раз такие вычислители калькуляторы моделей
TN
там главное предикативность и импредикативность рулить и вселенных побольше
TN
(как я думаю)
NK
J это экстенсиональность
TN
J это просто элиминатор, предикативная форма транспорта зависимой функции
NK
о Fix я промолчу, там его надо хитро добавлять чтобы индукция не пропадала
TN
его можно смоделировать и категорно
TN
вот встроить нельзя, да
TN
втроить можно только имея гомотопический отрезок
TN
но это уже не MLTT даже
NK
но на самом деле непонятно что из этого эссеншиал
NK
и в этом суть нашей работы разобраться что "просто элиминатор" а что не просто!
NK
у меня как раз есть. Я вот не уверен что текущие кубические кан-сеты или как их там это минимум для натуральных :) Ну и сам cubicaltt там же 100500 примитивов
NK
ща посчитаем
TN
я уже посчитал
TN
data O5 = O4
| Path: O5 → O5 → O4
| PathLam: Binder → O5 → O5 → O5
| PathApp: O5 → Formula → O5 → O5
| Comp: O5 → O5 → O5
| Fill: O5 → O5 → O5
| Glue: O5 → O5 → O5
| GlueElem: O5 → O5 → O5
| UnGlueElem: O5 → O5 → O5
| Path: O5 → O5 → O4
| PathLam: Binder → O5 → O5 → O5
| PathApp: O5 → Formula → O5 → O5
| Comp: O5 → O5 → O5
| Fill: O5 → O5 → O5
| Glue: O5 → O5 → O5
| GlueElem: O5 → O5 → O5
| UnGlueElem: O5 → O5 → O5
TN
вот HTS
TN
Path, PathLam, PathApp — нельзя удалить
Comp — нельзя удалить, Fill — вроде можно
Glue,GlueElem,UnglueElem — нельзя вроде удалить, UA, IsoPath перестают работать
Comp — нельзя удалить, Fill — вроде можно
Glue,GlueElem,UnglueElem — нельзя вроде удалить, UA, IsoPath перестают работать