Assistant Professor in the School of Philosophy at Zhejiang University, China.
mpl. A Henkin-style completeness proof for the modal logic S5
ipl. Lean
hott-book-in-lean. Formalization of the Part I of the Homotopy Type Theory book in Lean 2
cubo. Cubo is an experimental proof assistant for cubical extensional type theory
