Rzk: a Proof Assistant for Synthetic $\infty$-Categories

Nikolai Kudasov, Violetta Sim, Benedikt Ahrens

Homotopy type theory (HoTT) is a type theory that allows for synthetic reasoning about $\infty$-groupoids. Several proof assistants (such as Rocq and Agda) implement variants of Ho…