![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Крайне интересная публикация
Mar. 14th, 2016 02:28 pmОригинал взят у ![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
akuklev в Крайне интересная публикация
akuklev в Крайне интересная публикацияhttp://www.cs.ru.nl/~herman/PUBS/FibDialg.pdf
(Вместо того, чтобы взять базовую MLTT (Π+Σ) и обогащать её терминальным и инициальным типами, натуральными числами, индуктивными типами всё более возрастающей сложности, вселенными и т.д., можно сделать теорию типов из всего двух first-class компонентов: индуктивных типов и коиндуктивных типов. И уже в их терминах можно уже определить всё остальное. Точнее, пока это только первый шаг, как делать Π и Σ уже понятно, а вот как готовить Id-типы и (унивалентные) вселенные ещё непонятно.)
(Вместо того, чтобы взять базовую MLTT (Π+Σ) и обогащать её терминальным и инициальным типами, натуральными числами, индуктивными типами всё более возрастающей сложности, вселенными и т.д., можно сделать теорию типов из всего двух first-class компонентов: индуктивных типов и коиндуктивных типов. И уже в их терминах можно уже определить всё остальное. Точнее, пока это только первый шаг, как делать Π и Σ уже понятно, а вот как готовить Id-типы и (унивалентные) вселенные ещё непонятно.)
