Rzk: A Proof Assistant for Synthetic ∞-Categories

Programming Languages(arxiv.org)view on HackerNews
proof assistantsynthetic infinity-categoriestype theoryRSTTRzk

Author: Jimmc414

Date: 7/15/2026

Article Summary:
The paper presents Rzk, a proof assistant for synthetic reasoning about ∞-categories, a refinement of Riehl and Shulman's simplicial type theory.