Rzk Proof Assistant and Simplicial HoTT Formalisation

Invited seminar talk · STEP — russian seminar on Software Engineering, Theory and Experimental Programming · · Novosibirsk, Russia (hybrid) · delivered in Russian

A Russian-language STEP seminar talk introducing rzk as an experimental proof assistant for synthetic ∞-category theory, and demonstrating early formalisations. Delivered several months before the English-language HoTTEST 2023 talk.

Video Recording

Slides