Mar. 14th, 2016

akuklev: (ДР Цертуса 2011)
http://www.cs.ru.nl/~herman/PUBS/FibDialg.pdf

(Вместо того, чтобы взять базовую MLTT (Π+Σ) и обогащать её терминальным и инициальным типами, натуральными числами, индуктивными типами всё более возрастающей сложности, вселенными и т.д., можно сделать теорию типов из всего двух first-class компонентов: индуктивных типов и коиндуктивных типов. И уже в их терминах можно уже определить всё остальное. Точнее, пока это только первый шаг, как делать Π и Σ уже понятно, а вот как готовить Id-типы и (унивалентные) вселенные ещё непонятно.)

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 28th, 2017 04:43 pm
Powered by Dreamwidth Studios