rzk — an experimental proof assistant for synthetic ∞-categories

rzk is an early prototype of a proof assistant for a family of type systems, including Riehl and Shulman's «Type Theory for Synthetic ∞-categories» (https://arxiv.org/abs/1705.07442).