Towards Formalization of Directed Univalence in Rzk Proof Assistant
A work-in-progress report on formalising Triangulated Type Theory in rzk. We extend the proof assistant with a general mode-parametric framework for modalities, instantiate it to obtain the discrete, codiscrete, and opposite modalities of Triangulated Type Theory, and use them to construct the universe of groupoid types and to establish the maps that together yield directed univalence.
Code: rzk-lang/rzk (lishy2-modal), LIshy2/sHoTT (diruniv)
Talipov, I., Kudasov, N. (2026). "Towards Formalization of Directed Univalence in Rzk Proof Assistant." HoTT/UF 2026 — Workshop on Homotopy Type Theory / Univalent Foundations, Aarhus, Denmark.