Martin-Löf, Intuitionistic Type Theory.
Организатор: @orenty7

Продолжаем погружаться в MLTT. Мы уже видели мотивацию и правила вывода в "Constructive mathematics and computer programming", теперь разберём их подробнее.

Прочитать статью к воскресенью, 28 июня. Встречаемся на нашем дискорд-сервере в 19:00 по Москве.

Статья в первом комменте.
Формат | Методы доступа в дискорд