Как писать математику используя систему Кок I

Кок - это программа, которая предоставляет набор инструментов для эффективной работы с формальными рассуждениями в современной (зависимой, полиморфной) теории типов.
На основании таких теорий типов сформулированы унивалентные основания, в которых примитивными объектами являются не множества, а бесконечность-групойды или, эквивалентно, гомотопические типы.
Поэтому, используя Кок, можно "писать" унивалентную математику в такой форме, что правильность рассуждений проверяется компьютером.
Я покажу часть имеющейся у нас сейчас библиотеки конструкций, включая конструкцию локализации коммутативных колец, и мы попробуем в классе построить конструкцию спектров коммутативных колец.
Студентам будет полезно посмотреть статью Experimental library of univalent formalization of mathematics, а также скачать и установить программу Кок.