Readings on computational logic, interactive theorem proving and functional programming.

Simple theorem prover for the tope layer of Riehl and Shulman type theory with shapes.

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

Formalisations for simplicial HoTT and synthetic ∞-categories.

HoTT Book formalisations in Rzk.