STEP24may23NikolaiKudasov

Николай Дмитриевич Кудасов (Университет Иннополис): Rzk Proof Assistant and Simplicial HoTT Formalisation
Аннотация: Rzk is an experimental proof assistant for synthetic infinity-categories. This project has started with the idea of bringing Riehl and Shulman's 2017 to "life" by implementing a proof assistant based on their type theory with shapes. An early prototype with an online playground is available. Perhaps, the largest formalizations are available in two related projects done in collaboration with Emily Riehl and Jonathan Weinberger: https://github.com/fizruk/sHoTT and https://github.com/emilyriehl/yoneda(... is external). In this talk, I will introduce the proof assistant, demonstrate some of its features, and briefly go over available formalizations. (Early prototype of a proof assistant is available at https://fizruk.github.io/rzk/)