Frex: dependently-typed algebraic simplification. - Guillaume Allais; Edwin C. Brady; Nathan Corbyn; Ohad Kammar; Jeremy Yallop (CoRR, 2023)

homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. - Nathan Corbyn; Lukas Heidemann; Nick Hu; Chiara Sarti; Calin Tataru; Jamie Vicary (FSCD, 2024)