Rzk proof assistant and simplicial HoTT formalization
An invited HoTTEST talk introducing rzk — a proof assistant for the simplicial extension of homotopy type theory by Riehl and Shulman — alongside the ∞-categorical Yoneda lemma formalisation (joint work with Emily Riehl and Jonathan Weinberger).