3. Computational Content of Type Theories

Вот тут есть список более или менее всех разумных textbooks по тематике:
https://github.com/steshaw/plt

Чтобы понять, что достигнуто (а достигнута computational interpretation of univalence без многих ценных эта-правил) нужно разобраться с
https://github.com/mortberg/cubicaltt

Чтобы понять, зачем полезны эта-правила можно посмотреть презентацию Андреаса Абеля
http://www2.tcs.ifi.lmu.de/~abel/talkAIM09.pdf, где он показывает как штуки которые очевидно должны работать не тайпчекаются, если язык не поддерживает eta-expansion для record types. Вычислительная реализация большего количества эта-правил позволяет чтобы тайпчекалось большее количество корректных по-существу термов. Конор МакБрайд с Торстеном Альтенкирхом поставили очень высокую планку возможного, сформулировав (см. статьи Towards Observational Type Theory и Observational Equality Now) расширение ITT, в котором вычислительно реализованы эта правила не только для record types, но вообще для всех индуктивных типов, включая Id-типы. (Туда, кстати, ещё можно добавить вычислительных правил для полного экстаза, см. New Equations for Neutral Terms.)

Наличие эта-правила для Id-типов позволяет делать очень удобный паттерн матчинг (см. статью Конора dependent pattern matching elimination). В HoTT эта-правило Id-типов ослабляется до J rule, однако если J rule работает вычислительно, жить всё ещё хорошо и приятно (см. статью Pattern Matching Without K), но так как в cubicaltt J-правило вычислительно не работает, dependent pattern-matching там можно делать только через тактики, как в Coq'е, что замутняет доказательства и всячески осложняет жизнь по мелочам.