A Coq library for Homotopy Type Theory

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

An axiom-free formalization of category theory in Coq for personal study and practical work

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

A foundational framework for modular cryptographic proofs in Coq

HoTT proofs using experimental induction-induction (mostly about real numbers) (used to contain the HoTT.Classes proofs)

Linear Algebra