Towards Univalent Construction Calculus

[akuklev]

Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning

Comments

[nponeccop]

Так а чо там на ниве computational HoTTs происходит? Есть что интересное свежее почитать? А то как Максим засел за диссертацию, так я как-то и потерял нить происходящего.

[akuklev]

Меня почитайте :)

https://akuklev.github.io/HOCC/ - черновики конечно ещё далеки до публикации, но там много интересного.

[nponeccop]

Отличное чтиво

[akuklev]

Спасибо!